Source/Reference

Float32Exact

reference/numeric/Float32Exact.alpha

141 lines17 declarations6.3 KiBSHA-256 a0bb801f503e

def · lines 14–15

float32NotRounded

Full file
binary32 constants from their exact values. Each is the binary32 nearest the value, computed by these functions with unbounded naturals -- the executable's naturals are 64-bit words and these exact values are not -- so a plan takes a constant as `(compile-time (derivation))`: the compiler evaluates it and hands the program the word. pi and ln 2 are bounded to 40 places, enough that both ends of their interval round alike.
14def float32NotRounded : Nat =
15  0x7fc0dead

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.