lean4-htt/tests/lean/1207.lean.expected.out
2017-05-14 19:40:36 -07:00

2 lines
95 B
Text

1207.lean:15:2: error: unknown identifier 'h'
1207.lean:21:23: error: unknown identifier 'foo'