def or_false_left

stelliferous@0.0.2.0 · proofs/boolean_logic.bend:81

import stelliferous@0.0.2.0/proofs/boolean_logic.bend as BooleanLogic
import Base
import stelliferous@0.0.2.0/proofs/word_encoding.bend as WordEncoding

81def or_false_left(+first: Bool,+second: Bool,proof: {first || second == False{} : Bool}) -> {first == False{} : Bool}:
82  match first:
83    case False{}: {==}
84    case True{}: Empty.absurd({True{} == False{} : Bool},WordEncoding.false_true(Equal.sym(Bool,True{},False{},proof)))

Uses (5)

Used by (0)

No other definition uses this definition.