updated plan
This commit is contained in:
parent
ad9e54a7f5
commit
2b441fe0ec
15
README.md
15
README.md
|
@ -3,15 +3,16 @@ A dependently typed system
|
||||||
|
|
||||||
# TODO
|
# TODO
|
||||||
|
|
||||||
* Inductively defined datatypes
|
* Some fun types
|
||||||
|
* ⊤
|
||||||
|
* ⊥
|
||||||
|
* ℕ
|
||||||
|
* Σ
|
||||||
|
* Id
|
||||||
|
|
||||||
* Implicit arguments, Metavariables, and Unification
|
* Implicit arguments
|
||||||
|
|
||||||
* Universe hierarchy
|
* Universes
|
||||||
|
|
||||||
* Universe Polymorphism
|
|
||||||
|
|
||||||
* Cumulative Universes(?)
|
|
||||||
|
|
||||||
# References
|
# References
|
||||||
|
|
||||||
|
|
Loading…
Reference in New Issue
Block a user