def ldz_c

bend-collections-laws-math@1.0.0.0 · proofs/math/typed/f64exp.bend:237

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

237def ldz_c(+x: F.F64, +neg: Bool, +k: Nat, +iz: Bool) -> {F.ld_z(x, F.Exp{neg, k}, iz) == SF.pick(F.F64, iz, x, LD(x, neg, k)) : F.F64}:
238  match iz:
239    case True{}:
240      {==}
241    case False{}:
242      ldf_c(x, neg, k)