diff --git a/README.md b/README.md index 3ae90e2..261d7b4 100644 --- a/README.md +++ b/README.md @@ -3,15 +3,16 @@ A dependently typed system # TODO -* Inductively defined datatypes +* Some fun types + * ⊤ + * ⊥ + * ℕ + * Σ + * Id -* Implicit arguments, Metavariables, and Unification +* Implicit arguments -* Universe hierarchy - - * Universe Polymorphism - - * Cumulative Universes(?) +* Universes # References