3 ms·
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
by ahelwer 7y ago
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 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.