#exit not supported
Opened this issue · 2 comments
nomeata commented
After pasting some unsupported file and crashing lean I tried to use #exit to make it ignore the rest of the files, as I would do with normal lean, but it seems it doesn’t work like that.
If easily possible, it would be nice to have this supported.
david-christiansen commented
Can you paste an example of the program that you'd like to write here?
nomeata commented
Sorry; it was basically #2 with #exit after the first paragraph. The idea was that I'd like to be able to paste a big chunk of text, possibly with syntax error and other, and then fix it up bit by bit, moving the #exit down as I go.
Buy not very important, it was just something I happen to have tried.