The untyped / simply typed / dependently typed lambda calculus & friends, implemented via Normalization by Evaluation.
- Lean 100%
| NbE | implement ToString for tartlet | |
| .gitignore | init | |
| lakefile.toml | initial implementation of tartlet (probably buggy!!) | |
| lean-toolchain | init | |
| Main.lean | init | |
| NbE.lean | initial implementation of tartlet (probably buggy!!) | |
| README.md | initial implementation of tartlet (probably buggy!!) | |
NbE: Normalization by Evaluation (scraps)
An implementation of a variety of languages, from the untyped lambda calculus to a tiny dependently-typed language (Tartlet), in Lean.
This follows David Thrane Christiansen's Checking Dependent Types with Normalization by Evaluation tutorial.
This code was mostly written when I was first learning Lean. It should not be taken as idiomatic!