def TN

bend-collections-laws-math@1.0.0.0 · proofs/math/typed/f64conv.bend:39

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/num.bend as NE

39# the spec's verdict on a nonnegative-or-zero integer part n with sign s
40def TN(+s: Bool, +n: Nat) -> Result<&2, &2, NE.NumError, Nat>:
41  SF.pick(Result<&2, &2, NE.NumError, Nat>, Bool.or(Bool.and(s, Bool.not(Nat.is_eq(n, 0n))), Bool.not(C.fits(64n, n))), Fail{NE.Overflow{}}, Done{n})