2023-10-29 00:07:15 +02:00
|
|
|
# Lean learning
|
|
|
|
|
|
|
|
|
|
This directory contains the results of my first adventure into the world of Lean 4.
|
|
|
|
|
|
|
|
|
|
## File structure
|
|
|
|
|
|
2023-10-29 01:15:32 +02:00
|
|
|
| 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 |
|
