non_exhaustive_error.lean:2:4: error: non-exhaustive match, the following cases are missing:
g (1, _)
g (nat.succ (nat.succ _), _)
non_exhaustive_error.lean:2:0: warning: declaration 'g' uses sorry
non_exhaustive_error.lean:6:11: error: non-exhaustive match, the following cases are missing:
f "hello world" _
f _ _
non_exhaustive_error.lean:6:0: warning: declaration 'f' uses sorry
non_exhaustive_error.lean:10:4: error: non-exhaustive match, the following cases are missing:
foo (nat.succ _) 1
non_exhaustive_error.lean:10:0: warning: declaration 'foo' uses sorry
non_exhaustive_error.lean:17:11: error: non-exhaustive match, the following cases are missing:
f 0 (nat.succ _)
f (nat.succ _) _
g 0 (nat.succ _)
g (nat.succ _) _
non_exhaustive_error.lean:17:0: warning: declaration 'f.g' uses sorry
non_exhaustive_error.lean:27:4: error: non-exhaustive match, the following cases are missing:
const_name (_nest_1_1._nest_1_1.term._mut_.mk_0 _ (term.pack_0_1 (_nest_1_1._nest_1_1.term._mut_.mk_0 _ _ :: _)))
non_exhaustive_error.lean:27:0: warning: declaration 'const_name' uses sorry
non_exhaustive_error.lean:31:4: error: non-exhaustive match, the following cases are missing:
f _
non_exhaustive_error.lean:31:0: warning: declaration 'other2.f' uses sorry
non_exhaustive_error.lean:34:4: error: non-exhaustive match, the following cases are missing:
g _
non_exhaustive_error.lean:34:0: warning: declaration 'other2.g' uses sorry
non_exhaustive_error.lean:37:9: error: non-exhaustive match, the following cases are missing:
h _
non_exhaustive_error.lean:40:4: error: non-exhaustive match, the following cases are missing:
r _
non_exhaustive_error.lean:40:0: warning: declaration 'other2.r' uses sorry
