From 4f62d70a1a64564ce370d8ecd748719204753fec Mon Sep 17 00:00:00 2001
From: yohlo <yohlerkyle@gmail.com>
Date: Fri, 18 Sep 2026 23:10:37 -0700
Subject: [PATCH] docs: add materials draft

---
 README.md    |  3 ---
 materials.md | 19 +++++++++++++++++++
 2 files changed, 19 insertions(+), 3 deletions(-)
 create mode 100644 materials.md

diff --git a/README.md b/README.md
index 57ef8eb..5bdbfe9 100644
--- a/README.md
+++ b/README.md
@@ -1,5 +1,2 @@
 # elab
-
----
-
 Learning outline
\ No newline at end of file
diff --git a/materials.md b/materials.md
new file mode 100644
index 0000000..93efb85
--- /dev/null
+++ b/materials.md
@@ -0,0 +1,19 @@
+# Materials
+
+### Books
+
+- Types and Programming Languages by Benjamin C. Pierce
+- Functional Programming in Lean by David Thrane Christiansen
+- Crafting Interpreters by Robert Nystrom (https://craftinginterpreters.com)
+- Certified Programming with Dependent Types by Adam Chlipala (http://adam.chlipala.net/cpdt/)
+- Essentials of Compilation by Jeremy G. Siek (https://github.com/IUCompilerCourse/Essentials-of-Compilation)
+- Theorem Proving in Lean 4 by Jeremy Avigad, Leonardo de Moura, Soonho Kong, Sebastian Ullrich (https://lean-lang.org/theorem_proving_in_lean4/)
+
+
+### Other
+
+- Software Foundations — https://softwarefoundations.cis.upenn.edu
+- Natural Number Game — https://adam.math.hhu.de
+- Z3 guide — https://microsoft.github.io/z3guide/
+- z3-solver — https://github.com/Z3Prover/z3
+- ts-pattern — https://github.com/gvergnaud/ts-pattern