lean2/tests/lean/quot_bug.lean.expected.out
2015-04-29 10:01:17 -07:00

2 lines
59 B
Text

λ (x : A), f x
quot_bug.lean:8:59: warning: using 'sorry'