From 0d1e3638fe561754ba542950fd9a1d5a87ae51cd Mon Sep 17 00:00:00 2001 From: Matei Adriel Date: Sun, 29 Oct 2023 00:07:15 +0200 Subject: [PATCH] Document lean experiments --- idris/learning/README.md | 2 +- lean/learning/LeanSandbox.lean | 1 - lean/learning/Learning.lean | 1 + lean/learning/{LeanSandbox => Learning}/Integers.lean | 2 +- lean/learning/{LeanSandbox => Learning}/Nat.lean | 0 lean/learning/{LeanSandbox => Learning}/Noob.lean | 0 lean/learning/Main.lean | 2 +- lean/learning/README.md | 11 +++++++++++ lean/learning/lakefile.lean | 2 +- 9 files changed, 16 insertions(+), 5 deletions(-) delete mode 100644 lean/learning/LeanSandbox.lean create mode 100644 lean/learning/Learning.lean rename lean/learning/{LeanSandbox => Learning}/Integers.lean (99%) rename lean/learning/{LeanSandbox => Learning}/Nat.lean (100%) rename lean/learning/{LeanSandbox => Learning}/Noob.lean (100%) create mode 100644 lean/learning/README.md diff --git a/idris/learning/README.md b/idris/learning/README.md index 4e9db93..2b7e661 100644 --- a/idris/learning/README.md +++ b/idris/learning/README.md @@ -1,6 +1,6 @@ # Idris learning -This directory contains my experiments when first learning idris. +This directory contains the results of my first adventure into the world of Idris 2. ## File structure diff --git a/lean/learning/LeanSandbox.lean b/lean/learning/LeanSandbox.lean deleted file mode 100644 index e99d3a6..0000000 --- a/lean/learning/LeanSandbox.lean +++ /dev/null @@ -1 +0,0 @@ -def hello := "world" \ No newline at end of file diff --git a/lean/learning/Learning.lean b/lean/learning/Learning.lean new file mode 100644 index 0000000..99415d9 --- /dev/null +++ b/lean/learning/Learning.lean @@ -0,0 +1 @@ +def hello := "world" diff --git a/lean/learning/LeanSandbox/Integers.lean b/lean/learning/Learning/Integers.lean similarity index 99% rename from lean/learning/LeanSandbox/Integers.lean rename to lean/learning/Learning/Integers.lean index d984d58..3133ea1 100644 --- a/lean/learning/LeanSandbox/Integers.lean +++ b/lean/learning/Learning/Integers.lean @@ -1,4 +1,4 @@ -import LeanSandbox.Nat +import Learning.Nat macro "nat_ring_all" : tactic => `(simp_all [Nat.mul_assoc, Nat.mul_comm, Nat.mul_left_comm, Nat.add_assoc, Nat.add_left_comm, Nat.add_comm, Nat.left_distrib, Nat.right_distrib]) macro "nat_ring" : tactic => `(simp [Nat.mul_assoc, Nat.mul_comm, Nat.mul_left_comm, Nat.add_assoc, Nat.add_left_comm, Nat.add_comm, Nat.left_distrib, Nat.right_distrib]) diff --git a/lean/learning/LeanSandbox/Nat.lean b/lean/learning/Learning/Nat.lean similarity index 100% rename from lean/learning/LeanSandbox/Nat.lean rename to lean/learning/Learning/Nat.lean diff --git a/lean/learning/LeanSandbox/Noob.lean b/lean/learning/Learning/Noob.lean similarity index 100% rename from lean/learning/LeanSandbox/Noob.lean rename to lean/learning/Learning/Noob.lean diff --git a/lean/learning/Main.lean b/lean/learning/Main.lean index f42a224..1b7ecfd 100644 --- a/lean/learning/Main.lean +++ b/lean/learning/Main.lean @@ -1,4 +1,4 @@ -import LeanSandbox +import Learning def main : IO Unit := IO.println s!"Hello, {hello}!" diff --git a/lean/learning/README.md b/lean/learning/README.md new file mode 100644 index 0000000..44b4a36 --- /dev/null +++ b/lean/learning/README.md @@ -0,0 +1,11 @@ +# 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 | diff --git a/lean/learning/lakefile.lean b/lean/learning/lakefile.lean index ddc3fb0..ee0ed78 100644 --- a/lean/learning/lakefile.lean +++ b/lean/learning/lakefile.lean @@ -1,6 +1,6 @@ import Lake open Lake DSL -package «lean-sandbox» { +package «lean-learning» { -- add configuration options here }