def isclose_value

bend-collections-laws-math@1.0.0.0 · proofs/math/typed/f64close.bend:88

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/src/math/num.bend as NE
import bend-collections-laws-math@1.0.0.0/proofs/math/typed/f64cmp.bend as FC

88def isclose_value(+a: F.F64, +b: F.F64, +rel: F.F64, +at: F.F64) -> SF.IsClose.value(a, b, rel, at):
89  +z = F.zero(False{})
90  +e1 = Equal.cong(Bool, Result<&2, &2, NE.NumError, Bool>, t => F.ic_tol(a, b, rel, at, Bool.or(t, F.lt(at, z))), F.lt(rel, z), SF.lt_s(rel, z), FC.lt_value(rel, z))
91  +e2 = Equal.cong(Bool, Result<&2, &2, NE.NumError, Bool>, t => F.ic_tol(a, b, rel, at, Bool.or(SF.lt_s(rel, z), t)), F.lt(at, z), SF.lt_s(at, z), FC.lt_value(at, z))
92  +r1 = F.ic_tol(a, b, rel, at, Bool.or(SF.lt_s(rel, z), F.lt(at, z)))
93  +r2 = F.ic_tol(a, b, rel, at, Bool.or(SF.lt_s(rel, z), SF.lt_s(at, z)))
94  Equal.trans(Result<&2, &2, NE.NumError, Bool>, F.isclose(a, b, rel, at), r1, SF.isclose(a, b, rel, at), e1, Equal.trans(Result<&2, &2, NE.NumError, Bool>, r1, r2, SF.isclose(a, b, rel, at), e2, itol(a, b, rel, at, Bool.or(SF.lt_s(rel, z), SF.lt_s(at, z)))))