lean4web
lean4web copied to clipboard
leanprover-community
The Lean 4 web editor
How feasible is it to add the vim motions feature? Some web editors support it like [replit](https://replit.com/) has these `keybinds` option:  It would widely improve the usability of the...
When clicking on the Examples / Load menus, the hamburger menu opens as well.
The remaining part about changing lean projects is that after changing project (i.e. lean version) the editor messages (squigglies, yellow task bar, ...) do not update unless the site is...
Ideally, all projects should import the `Webeditor` package, so they get access to `#package_version`. For this, it needs to be a separate repo.
`bubblewrap` seems to be the major limiting factor that this cannot be run on anything but linux. Probably would be good to default to not using `bubblewrap` if it does...
Example, where the comment highlighting is off: [demo](https://lean.math.hhu.de/#code=%2F-%20%23%23%20Wichtig%3A%0A-%20Bei%20der%20Verwendung%20von%20%60calc%60%20müssen%20alle%20%60_%60%20gleich%20weit%20eingerückt%20sein%2C%20sonst%20gibt%20es%0A%20%20verwirrende%20Fehlermeldungen.%0A-%20Sehen%20Sie%20die%20Fehlermeldung%20%60fail%20to%20show%20termination%20for%20...%60%3F%20Das%20weist%20darauf%20hin%2C%20dass%0A%20%20Induktion%20verwendet%20wurde%2C%20die%20Argumente%20aber%20nicht%20strukturell%20kleiner%20sind.%20Eventuell%20wurden%0A%20%20in%20Kombination%20mit%20%60rw%60%20auch%20Argumente%20nicht%20explizit%20angegeben%3F%20-%2F%0A) ``` /- ## Wichtig: - Bei der Verwendung von `calc` müssen alle `_` gleich weit eingerückt sein, sonst gibt es verwirrende Fehlermeldungen....
On mobile I can't paste code, nor can I select code in the editor to copy it.
Would be nice to have go-to-def open the correct page of the docs: https://leanprover-community.github.io/mathlib4_docs/
```lean #eval (panic "oh no" : Nat) ```