def ofz

bend-collections-laws-math@1.0.0.0 · proofs/math/typed/f64ofnat.bend:95

import Base
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
import bend-collections-laws-math@1.0.0.0/src/math/natural.bend as M

95def ofz(+n: Nat, +z: Bool, +hz: {Nat.is_eq(n, 0n) == z : Bool}) -> {F.of_nat_z(n, z) == SF.round(False{}, n, SF.zb()) : F.F64}:
96  match z:
97    case True{}:
98      Equal.sym(F.F64, SF.round(False{}, n, SF.zb()), SF.zero(False{}), Equal.cong(Bool, F.F64, t => SF.pick(F.F64, t, SF.zero(False{}), SF.round_u(False{}, n, SF.zb(), Nat.max(Nat.sub(Nat.add(SF.zb(), M.bit_length(n)), 53n), Nat.sub(SF.zb(), 1074n)))), Nat.is_eq(n, 0n), True{}, hz))
99    case False{}:
100      on_c(n, hz, Nat.is_le(M.bit_length(n), 63n), {==})