BooleanLogic.choose_matching: def of stelliferous@0.0.2.0
Import: import stelliferous@0.0.2.0/proofs/boolean_logic.bend as BooleanLogic
Lines 12-19 of stelliferous@0.0.2.0/proofs/boolean_logic.bend: https://jend.leeeet.dev/read.txt?path=stelliferous@0.0.2.0/proofs/boolean_logic.bend&start_line=12&end_line=19

import Base

def choose_matching(-Element: Data,+first: Bool,+rest: Bool,+actual: Element,+wanted: Element,+old: Element,
  correct: When(first,{actual == wanted : Element})) ->
  {Bool.pick(Element,rest,wanted,Bool.pick(Element,first,actual,old)) == Bool.pick(Element,first || rest,wanted,old) : Element}:
  match first rest:
    case False{} False{}: {==}
    case False{} True{}: {==}
    case True{} False{}: correct
    case True{} True{}: {==}

Uses (4):
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Bool
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Bool.or
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Bool.pick
  https://jend.leeeet.dev/definition.txt?path=stelliferous@0.0.2.0/proofs/boolean_logic.bend&name=When