def ee_c

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

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

126def ee_c(+t: Nat, +c: Bool) -> {F.exp_pick(t, c) == SF.pick(F.Exp, c, F.Exp{False{}, Nat.sub(t, 3000n)}, F.Exp{True{}, Nat.sub(3000n, t)}) : F.Exp}:
127  match c:
128    case True{}:
129      {==}
130    case False{}:
131      {==}