do_match_fail.lean:8:2: error: match failed
state:
p q : Prop,
a : p,
a_1 : q
⊢ p
do_match_fail.lean:20:3: error: non-exhaustive match, the following cases are missing:
_example._match_1 list.nil
do_match_fail.lean:18:0: warning: declaration '[anonymous]' uses sorry
