def or_cases

minebender-game@1.0.0.0 · proof_solver.bend:1945

import Base

1945def or_cases(+a: Bool, +b: Bool, e: {Bool.or(a, b) == True{} : Bool}) -> Or({a == True{} : Bool}, {b == True{} : Bool}):
1946  match a:
1947    case True{}:
1948      Inl{{==}}
1949    case False{}:
1950      Inr{e}