.. | ||
Learning | ||
.gitignore | ||
lakefile.lean | ||
Learning.lean | ||
Main.lean | ||
README.md |
Lean learning
This directory contains the results of my first adventure into the world of Lean 4.
File structure
File | Description |
---|---|
Noob.lean | Syntax practice |
Nat.lean | Natural numbers |
Integers.lean | Integers as quotient types over differences of naturals |