def ok_ix

bend-collections-laws-math@1.0.0.0 · proofs/math/typed/f64fmod.bend:519

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/f64cmp.bend as FC

519def ok_ix(+x: F.F64, +y: F.F64, +h: {SF.rbad(x, y) == False{} : Bool}) -> {SF.is_inf(x) == False{} : Bool}:
520  FC.or_r(Bool.not(SF.ordered(x, y)), SF.is_inf(x), FC.or_l(Bool.or(Bool.not(SF.ordered(x, y)), SF.is_inf(x)), SF.is_zero(y), h))