digama0/lean-type-theory
View on GitHub ↗ ★ 176 TeX
LaTeX code for a paper on lean's type theory
4 mentions on Hacker News by 4 people: 0 stories, 4 comments · first 2020-11-22 · latest 2025-08-03
20082026
-
…though, since there is no point in quotienting a proposition. [0] see the end of section 3.1 in https://github.com/digama0/lean-type-theory/releases/downloa...
comment by semolinapudding · 2025-08-03 · in Ongoing Lean formalization of the proof for Fermat's Last Theorem -
…as part of the Lean kernel) to u, but u doesn't have type A, and may not even type check. (See https://github.com/digama0/lean-type-theory/releases/downloa... Sec. 3.1 for a detailed discussion of this issue.) This is obviously quite bad,…
comment by zozbot234 · 2025-08-03 · in Ongoing Lean formalization of the proof for Fermat's Last Theorem -
Mario Carneiro’s MS Thesis has a good overview of the type theory and how it compares to Coq: https://github.com/digama0/lean-type-theory/releases/downloa...
comment by denotational · 2024-12-22 · in Rosetta 2 creator leaves Apple to work on Lean full-time -
…This paper on Lean's type theory dovetails nicely with any of the kernel implementations: https://github.com/digama0/lean-type-theory/releases/tag/v1.... Also this article is really neat, thanks OP. These kinds of visual representations…
comment by lakecresva · 2020-11-22 · in Untangling Mechanized Proofs