def sq_ok_eq

bend-collections-laws-math@1.0.0.0 · proofs/math/typed/float.bend:118

import Base
import bend-collections-laws-math@1.0.0.0/src/math/generic.bend as G
import bend-collections-laws-math@1.0.0.0/src/math/num.bend as N

118def sq_ok_eq(~T: Data, ~test: N.Test<T> -> Bool, ~mo: NoMulOver(~T, ~test), +c: Bool, +b: T) -> {G.sq_ok(~T, ~test, c, b, True{}) == True{} : Bool}:
119  match c:
120    case True{}:
121      %Equal.sym(Bool, test(N.MulOver{b, b}), False{}, mo(b, b)) : {Bool.and(True{}, Bool.not(_)) == True{} : Bool}
122      {==}
123    case False{}:
124      {==}