3 ms·
First let me point out that you can jump to any level at any time, so you lose your progress, but only in a weak sense, if you lose your browser tab. You do los
by kevinbuzzard 7y ago
First let me point out that you can jump to any level at any time, so you lose your progress, but only in a weak sense, if you lose your browser tab. You do lose your proofs though.
The natural number game was made by passing a repository which contains essentially nothing but Lean code, through this generic tool https://github.com/mpedramfar/Lean-game-maker https://github.com/mpedramfar/Lean-game-maker which makes the html pages from the Lean code. If there is anyone out there who understands the Lean game maker code (I don't, it was written by my co-author) and is interested in implementing some kind of client side storage then feel free to ping me either at my Imperial email address or at the Lean Zulip chat https://leanprover.zulipchat.com https://leanprover.zulipchat.com .
- ahelwer 7y agoDid you use a similar tool to make this mixed formal/informal presentation of the squeeze theorem? https://wwwf.imperial.ac.uk/~buzzard/docs/lean/sandwich.html https://wwwf.imperial.ac.uk/~buzzard/docs/lean/sandwich.html
- kevinbuzzard 7y agoI used Patrick Massot's Lean Formatter https://github.com/leanprover-community/format_lean https://github.com/leanprover-community/format_lean to make the Lean web page with the analysis theorem on, and Mohammad Pedramfar's Lean game maker was very much inspired by the code in the formatter.