Did you use a similar tool to make this mixed formal/informal presentation of th... | Hacker News

Hacker News .hnnew | past | comments | ask | show | jobs | submit

		ahelwer on April 8, 2020 \| parent \| context \| favorite \| on: Natural number game 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

kevinbuzzard on April 8, 2020 [–]

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.

Guidelines | FAQ | Lists | API | Security | Legal | Apply to YC | Contact