def tiny
bend-collections-laws-math@1.0.0.0 · proofs/math/typed/f64exp.bend:121
import bend-collections-laws-math@1.0.0.0/proofs/math/typed/f64exp.bend as F64exp
import Base
import bend-collections-laws-math@1.0.0.0/spec/lib/common.bend as C
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
121def tiny(+s: Bool, +m: Nat, +x: Nat, +hm: {C.fits(53n, m) == True{} : Bool}, +hx: {Nat.is_lt(x, 63n) == True{} : Bool}) -> {SF.round(s, m, x) == SF.zero(s) : F.F64}:
122 tiny_c(s, m, x, hm, hx, Nat.is_eq(m, 0n), {==})