diff --git a/README.md b/README.md
index 5405a98..c6c4e04 100644
--- a/README.md
+++ b/README.md
@@ -22,9 +22,19 @@ A dependently typed system
 
 * Martin-Löf Identity types
 
-# TODO
+# Lacking
 
-* Universes (a la tarksi)
+Here are some things which are *not* present but could be.
+
+This project has served me well by teaching me about typechecking dependently typed systems. It's likely that the features listed below will not be implemented as I'll move onto other projects and learn more about elaboration.
+
+
+* Universes 
+  * a la tarksi
+
+* Inductives
+  * W types
+  * Indexed inductives
 
 * Elaboration
   * Implicit arguments
@@ -32,19 +42,6 @@ A dependently typed system
     * Syntax level russel universes
     * Universe of all other universes? (universe polymorphism)
 
-* Inductives
-  * Indexed inductives
-
-## Things that could be fun to do sometime eventually
-
-* Pattern matching in elaborator
-
-* Write down the rules
-
-* Performence optimisation?
-
-* Compile to scheme
-
 # References
 
 Some of the material I found helpful in groking dependent type checking: