michael/lean2
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions
lean2/tests/lean/bad_end.lean.expected.out

2 lines
75 B
Text
Raw Normal View History

feat(frontends/lean): remove 'context' command
2015-04-22 18:32:02 +00:00
bad_end.lean:1:4: error: invalid 'end', there is no open namespace/section
Reference in a new issue Copy permalink