12 lines
641 B
Markdown
12 lines
641 B
Markdown
# Lean learning
|
|
|
|
This directory contains the results of my first adventure into the world of Lean 4.
|
|
|
|
## File structure
|
|
|
|
| File | Description |
|
|
| ----------------------------------------- | ------------------------------------------------------- |
|
|
| [Noob.lean](./Learning/Noob.lean) | Syntax practice |
|
|
| [Nat.lean](./Learning/Nat.lean) | Natural numbers |
|
|
| [Integers.lean](./Learning/Integers.lean) | Integers as quotient types over differences of naturals |
|