def dexp_value

bend-collections-laws-math@1.0.0.0 · proofs/math/typed/f64tools.bend:43

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/proofs/math/typed/f64light.bend as FL

43def dexp_value(+x: F.F64) -> {F.dexp(x) == SF.xexp(x) : Nat}:
44  match x:
45    case F.Bits{+xl, +xh}:
46      +e1 = Equal.cong(Nat, Nat, t => F.dexp_z(t, Nat.is_eq(t, 0n)), F.exp_field(F.Bits{xl, xh}), SF.efield(F.Bits{xl, xh}), FL.hea(xl, xh))
47      Equal.trans(Nat, F.dexp(F.Bits{xl, xh}), F.dexp_z(SF.efield(F.Bits{xl, xh}), Nat.is_eq(SF.efield(F.Bits{xl, xh}), 0n)), SF.xexp(F.Bits{xl, xh}), e1, dz(SF.efield(F.Bits{xl, xh}), Nat.is_eq(SF.efield(F.Bits{xl, xh}), 0n)))