~/jendhub

def not_false

bend-collections-laws-math@1.0.0.0 · proofs/math/typed/u32laws.bend:214

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

214def not_false(+b: Bool, +h: {Bool.not(b) == False{} : Bool}) -> {b == True{} : Bool}:
215  match b:
216    case True{}:
217      {==}
218    case False{}:
219      Empty.absurd({False{} == True{} : Bool}, true_ne_false(h))

Uses (4)

Used by (1)