def choose_matching

stelliferous@0.0.2.0 · proofs/boolean_logic.bend:12

import Base

12def choose_matching(-Element: Data,+first: Bool,+rest: Bool,+actual: Element,+wanted: Element,+old: Element,
13  correct: When(first,{actual == wanted : Element})) ->
14  {Bool.pick(Element,rest,wanted,Bool.pick(Element,first,actual,old)) == Bool.pick(Element,first || rest,wanted,old) : Element}:
15  match first rest:
16    case False{} False{}: {==}
17    case False{} True{}: {==}
18    case True{} False{}: correct
19    case True{} True{}: {==}