def exp_of

bend-collections-laws-crypto@1.0.0.0 · spec/math/f64.bend:408

import Base
import bend-collections-laws-crypto@1.0.0.0/src/math/f64.bend as F

408# t - Z as a signed exponent
409def exp_of(+t: Nat) -> F.Exp:
410  pick(F.Exp, Nat.is_le(zb(), t), F.Exp{False{}, Nat.sub(t, zb())}, F.Exp{True{}, Nat.sub(zb(), t)})