patricktree.me
forked from
danabra.mov/overreacted
my blog https://overreacted.io
typo
danabra.mov
+1
-1
public/lean-for-javascript-developers/index.md
+1
-1
public/lean-for-javascript-developers/index.md
···
840
840
| succ (n : Nat) : Nat
841
841
```
842
842
843
-
Who would've thought that numbers just a recursively generated enum?
843
+
Who would've thought that numbers are just a recursively generated enum?
844
844
845
845
Turns out, a language built with recursively defined types like this can express and prove facts like that the [area of a circle is π * r ^ 2](https://github.com/leanprover-community/mathlib4/blob/aac79004bad67a82c18ab7d39c609529f4159d6f/Archive/Wiedijk100Theorems/AreaOfACircle.lean#L81-L130), or that [it takes 23 people to exceed a 50% chance of same birthday](https://github.com/leanprover-community/mathlib4/blob/aac79004bad67a82c18ab7d39c609529f4159d6f/Archive/Wiedijk100Theorems/BirthdayProblem.lean#L65-L81), or that [you can't cube a cube](https://github.com/leanprover-community/mathlib4/blob/aac79004bad67a82c18ab7d39c609529f4159d6f/Archive/Wiedijk100Theorems/CubingACube.lean#L533-L546). But you can also write normal programs with it that compile to C. [Async/await](https://lean-lang.org/fro/roadmap/1900-1-1-the-lean-fro-year-3-roadmap/) is in the works.
846
846