# Lean learning

This directory contains the results of my first adventure into the world of Lean 4.

## File structure

| File                                                 | Description                                             |
| ---------------------------------------------------- | ------------------------------------------------------- |
| [./Learning/Noob.lean](./Learning/Noob.lean)         | Syntax practice                                         |
| [./Learning/Nat.lean](./Learning/Nat.lean)           | Natural numbers                                         |
| [./Learning/Integers.lean](./Learning/Integers.lean) | Integers as quotient types over differences of naturals |