def decb_if

lawful-fields@0.1.1.0 · proof_list.bend:443

import Base
import lawful-fields@0.1.1.0/defs.bend as F
import lawful-arrays@0.1.0.0/proof_base.bend as AB

443# 2^32 must never take part in a conversion (the checker would expand it), so
444# the bound stays a variable M and the law instantiates it.
445def decb_if(+n: Nat, b: Bool, hb: {b == True{} : Bool}) -> {F.decb.if(n, b) == Some{n} : Maybe<&2, Nat>}:
446  match b:
447    case True{}:
448      {==}
449    case False{}:
450      Empty.absurd({F.decb.if(n, False{}) == Some{n} : Maybe<&2, Nat>}, AB.false_ne_true(hb))