Document lean experiments

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
 

lean/learning/LeanSandbox.lean

@@ -1 +0,0 @@
-def hello := "world"

lean/learning/Learning.lean

@@ -0,0 +1 @@
+def hello := "world"

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])

lean/learning/Main.lean

@@ -1,4 +1,4 @@
-import LeanSandbox
+import Learning
 
 def main : IO Unit :=
   IO.println s!"Hello, {hello}!"

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 |

lean/learning/lakefile.lean

@@ -1,6 +1,6 @@
 import Lake
 open Lake DSL
 
-package «lean-sandbox» {
+package «lean-learning» {
   -- add configuration options here
 }