Jon Eugster
Jon Eugster
`FileMap.lines` is an array that seems to be manually managed to have the form `#[1, 2, ..., n-1, n-1]` with same length as `FileMap.positions`. Remove this structure field in favour...
`rw [lemma_wth_typo]` with a non-existing lemma yields a wrong error message.
Implement `ext?`, `ext1?` to show used extensionality lemmas, and `ext!?` to brute-force try all ext-lemmas. - `ext?` displays a tactic replacement suggestion that could replace the `ext`. The tactic sequence...
There are already some issues about this, which should be linked here in future. Some info displayed by lean is very confusing. Overwrite that behaviour or change it in Lean:...
It would be nice to have a button in each level that automatically creates a new question on Zulip: - in the new members stream - a title that contains...
Having two tabs open with the same level will overwrite the user's progress randomly with either of the two. In reality one of the tabs will have an empty proof,...
``` ./././Game.lean:94:0: warning: No world introducing else, but required by Trace ./././Game.lean:94:0: warning: No world introducing then, but required by Trace ./././Game.lean:94:0: warning: No world introducing clear, but required by...
Add functionality to get some user feedback: - easy option to open an github issue from any level - have the option of a final playground level in a world,...
Add an option that worlds can be marked as completed before finishing all levels. - In the level files (.lean) add a command `FinalLevel` which when added after `Level xy`...