def not_f

bend-collections-laws-math@1.0.0.0 · proofs/math/typed/f64round.bend:698

import Base
import bend-collections-laws-math@1.0.0.0/proofs/math/typed/u32laws.bend as LW

698def not_f(+b: Bool, +h: {Bool.not(b) == False{} : Bool}) -> {b == True{} : Bool}:
699  match b:
700    case True{}:
701      {==}
702    case False{}:
703      Empty.absurd({False{} == True{} : Bool}, LW.true_ne_false(h))