def is_integer_value

bend-collections-laws-math@1.0.0.0 · proofs/math/typed/f64next.bend:169

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
import bend-collections-laws-math@1.0.0.0/proofs/math/typed/f64tools.bend as T

169def is_integer_value(+x: F.F64) -> SF.IsInteger.value(x):
170  +c = Nat.is_le(3000n, F.dexp(x))
171  +e1 = Equal.cong(Nat, Bool, t => Bool.and(Nat.is_lt(t, 2047n), F.ii_fin(x, c)), F.exp_field(x), SF.efield(x), T.ea(x))
172  +e2 = Equal.cong(Bool, Bool, t => Bool.and(Nat.is_lt(SF.efield(x), 2047n), t), F.ii_fin(x, c), Bool.or(c, LZ(x)), iif_c(x, c))
173  +e3 = Equal.cong(Nat, Bool, t => Bool.and(Nat.is_lt(SF.efield(x), 2047n), Bool.or(Nat.is_le(3000n, t), LZ(x))), F.dexp(x), SF.xexp(x), T.dexp_value(x))
174  +b1 = Bool.and(Nat.is_lt(SF.efield(x), 2047n), F.ii_fin(x, c))
175  +b2 = Bool.and(Nat.is_lt(SF.efield(x), 2047n), Bool.or(c, LZ(x)))
176  +b3 = Bool.and(Nat.is_lt(SF.efield(x), 2047n), Bool.or(Nat.is_le(SF.zb(), SF.xexp(x)), LZ(x)))
177  Equal.trans(Bool, F.is_integer(x), b1, b3, e1, Equal.trans(Bool, b1, b2, b3, e2, e3))