A small programming language formally defined with a series of blog posts and Lean code.
The blog posts are available in English and Japanese. (I am not a native Japanese speaker but I tried my hand at translating.)
| Part | Title | en | ja |
|---|---|---|---|
| 1 | Integers and booleans | en | ja |
| 2 | Functions | en | ja |
| 3 | Product types | en | ja |
| 4 | Sum types | en | ja |
This uses Lean 3.4.2, even though the 'latest' version as of writing is Lean 4. This is because the docs for Lean 4 seem even more scarce than the docs for Lean 3, and I couldn't figure out how to do some stuff. In general, although Lean 4 is clearly the future, it seems like it's not totally ready for prime time yet. I'm excited for the future though!