Re:Natural number game
by ahelwer on Wednesday April 08, 2020 @11:11AM
(#22813632)
Did 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
[ Parent
| on HN ]
Re:Natural number game
by kevinbuzzard on Wednesday April 08, 2020 @11:19AM
(#22813674)
I used Patrick Massot's Lean Formatter 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.