From a3dff999e2ac82b43dcb6944159dcee584a36c31 Mon Sep 17 00:00:00 2001
From: depsterr <depsterr@protonmail.com>
Date: Thu, 28 Jul 2022 04:47:54 +0200
Subject: [PATCH] updated readme

---
 README.md | 21 ++++++++++++++-------
 1 file changed, 14 insertions(+), 7 deletions(-)

diff --git a/README.md b/README.md
index 2b43008..fae0104 100644
--- a/README.md
+++ b/README.md
@@ -20,19 +20,26 @@ A dependently typed system
 
 * Σ Types
 
-# TODO
+* Martin-Löf Identity types
 
-* Performence optimisation
-  * Parsing !!! (this is like 90% of the time currently lmao)
-  * Memoize normalisation and conversion somehow?
+# TODO
 
 * Universes
 
-* Implicit arguments
+* Elaboration
+  * Implicit arguments
+  * Universe family application
 
-* (indexed) inductive datatypes
+* Inductives
+  * Indexed inductives
 
-* Write down the rules (I'll not get this far)
+## Things that could be fun to do sometime eventually
+
+* Pattern matching in elaborator
+
+* Write down the rules
+
+* Performence optimisation?
 
 * Compile to scheme