lean2/tests/lean/errors2.lean.expected.out

2 lines
51 B
Text
Raw Permalink Normal View History

errors2.lean:8:11: error: unknown identifier 'foo'