def wd.bool_eq

bend-osdev-u32@0.1.0.0 · PROOF_order.bend:171

import Base

171def wd.bool_eq(x: Bool, y: Bool, +e: {Bool.cmp(x, y) == EQ{} : Cmp}) -> {x == y : Bool}:
172  match x y:
173    case False{} False{}:
174      {==}
175    case False{} True{}:
176      Empty.absurd({False{} == True{} : Bool}, ab.lt_eq(e))
177    case True{} False{}:
178      Empty.absurd({True{} == False{} : Bool}, ab.gt_eq(e))
179    case True{} True{}:
180      {==}