def sgn

bend-collections-laws-math@1.0.0.0 · proofs/math/typed/f64addg.bend:99

import Base
import bend-collections-laws-math@1.0.0.0/proofs/math/typed/natcmp.bend as NC

99# the sign of a difference of opposite signs
100def sgn(+sa: Bool, +sb: Bool, +h: {Bool.not(Bool.xor(sa, sb)) == False{} : Bool}) -> {Bool.not(sa) == sb : Bool}:
101  match sa sb:
102    case True{} True{}:
103      NC.absurd_tf({False{} == True{} : Bool}, Equal.sym(Bool, True{}, False{}, h))
104    case True{} False{}:
105      {==}
106    case False{} True{}:
107      {==}
108    case False{} False{}:
109      NC.absurd_tf({True{} == False{} : Bool}, Equal.sym(Bool, True{}, False{}, h))