diff --git a/README.md b/README.md new file mode 100644 index 0000000..33eee5c --- /dev/null +++ b/README.md @@ -0,0 +1,14 @@ +# pi +A dependently typed system + +# TODO + +* Inductively defined datatypes + +* Implicit arguments, Metavariables, and Unification + +* Universe hierarchy + + * Universe Polymorphism + + * Cumulative Universes(?)