Source/Reference

Float32Exact

reference/numeric/Float32Exact.alpha

141 lines17 declarations6.3 KiBSHA-256 a0bb801f503e

def · lines 133–134

float32TwoPiHigh

Full file
2 pi in two words (the second the nearest to what the first misses), and 1 / (2 pi): pi in [P, P + 1] / 10^40
133def float32TwoPiHigh : Nat =
134  (compile-time (float32ExactBetween (nat-multiply 2 float32PiDigits) float32Places (nat-multiply 2 (succ float32PiDigits)) float32Places))

The compiler supplied declaration spans and resolved links from this source snapshot. This page does not assert that this file belongs to a checked closure.