def non

bend-collections-laws-math@1.0.0.0 · proofs/math/typed/f64light.bend:38

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

38def non(+x: F.F64, +b: Bool) -> {F.nan_or(x, b) == SF.pick(F.F64, b, F.nan(), x) : F.F64}:
39  match b:
40    case True{}:
41      Equal.trans(F.F64, F.nan_or(x, True{}), F.nan(), SF.pick(F.F64, True{}, F.nan(), x), {==}, Equal.sym(F.F64, SF.pick(F.F64, True{}, F.nan(), x), F.nan(), FR.pk_t(F.F64, F.nan(), x)))
42    case False{}:
43      Equal.trans(F.F64, F.nan_or(x, False{}), x, SF.pick(F.F64, False{}, F.nan(), x), {==}, Equal.sym(F.F64, SF.pick(F.F64, False{}, F.nan(), x), x, FR.pk_f(F.F64, F.nan(), x)))