Skip to content

Commit dc7063d

Browse files
authored
Update README.md
1 parent edd9e2c commit dc7063d

File tree

1 file changed

+8
-2
lines changed

1 file changed

+8
-2
lines changed

README.md

Lines changed: 8 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -11,9 +11,15 @@ running on a web server, and not in the browser.
1111

1212
## Scope of lean4web
1313

14-
The main scope of `lean4web` is to provide an easy way to run [MWEs](https://leanprover-community.github.io/mwe.html) from [Zulip](https://leanprover.zulipchat.com) with the latest [Mathlib](https://github.com/leanprover-community/mathlib4) installed.
14+
* Provide a clean, minimalistic and easily accessible way to run some (smallish) Lean snippets
15+
* Provide a simple way to run [MWEs](https://leanprover-community.github.io/mwe.html) from [Zulip](https://leanprover.zulipchat.com) with the latest [Mathlib](https://github.com/leanprover-community/mathlib4) installed.
16+
* Provide a easy way to demonstrate some Lean code in talks/lecutres.
17+
* Provide a easy way for newcomers to doodle with Lean before installing it.
18+
* Provide a way to run some Lean code in a mobile context.
1519

16-
While `lean4web` looks very similar to VSCode with the [Lean4 extension](https://marketplace.visualstudio.com/items?itemName=leanprover.lean4) installed - and it reuses much of that code - `lean4web` does not claim to be feature complete.
20+
Currently, serious Lean code development and larger projects are considered out-of-scope. For these, it might be more suitable to look at a setup using Codespaces or Gitpot.
21+
22+
While `lean4web` looks very similar to VSCode with the [Lean4 extension](https://marketplace.visualstudio.com/items?itemName=leanprover.lean4) installed - and it reuses much of that code - `lean4web` does not claim to be feature complete.
1723

1824
## Contribution
1925

0 commit comments

Comments
 (0)