Widen the low sixteen wire bits without rounding. BF16 has the binary32
sign and exponent positions with seven explicit fraction bits; appending
sixteen zero fraction bits preserves signed zero, subnormals and payloads.
27def bfloat16WidenWord =
28 (lambda unrestricted half : Nat .
29 (naturalMultiply (naturalModuloUnchecked half (naturalPowerOfTwo 16))
30 (naturalPowerOfTwo 16)))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.