1
Fork 0
solar-conflux/lean/learning
2023-10-29 00:07:15 +02:00
..
Learning Document lean experiments 2023-10-29 00:07:15 +02:00
.gitignore Move stuff around + add lean and idris experiments 2023-10-29 00:02:10 +02:00
lakefile.lean Document lean experiments 2023-10-29 00:07:15 +02:00
Learning.lean Document lean experiments 2023-10-29 00:07:15 +02:00
Main.lean Document lean experiments 2023-10-29 00:07:15 +02:00
README.md Document lean experiments 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

File Description
./Learning/Noob.lean Syntax practice
./Learning/Nat.lean Natural numbers
./Learning/Integers.lean Integers as quotient types over differences of naturals