def mz

bend-collections-laws-math@1.0.0.0 · proofs/math/typed/f64conv.bend:123

import Base
import bend-collections-laws-math@1.0.0.0/spec/lib/common.bend as C
import bend-collections-laws-math@1.0.0.0/spec/math/f64.bend as SF
import bend-collections-laws-math@1.0.0.0/src/math/f64.bend as F

123# a double with scale at least Z is normal, so its significand is not zero
124# the significand at an abstract exponent-is-zero bit b: instantiated at
125# False, the hidden bit 2^52 is never evaluated
126def mz(+x: F.F64, +b: Bool, +hb: {Nat.is_eq(SF.efield(x), 0n) == b : Bool}) -> {Nat.is_eq(SF.mant(x), 0n) == Nat.is_eq(Nat.add(SF.frac(x), C.shift(52n, SF.b2n(Bool.not(b)))), 0n) : Bool}:
127  Equal.cong(Bool, Bool, t => Nat.is_eq(Nat.add(SF.frac(x), C.shift(52n, SF.b2n(Bool.not(t)))), 0n), Nat.is_eq(SF.efield(x), 0n), b, hb)