aboutsummaryrefslogtreecommitdiff
path: root/HoTT.thy (follow)
Commit message (Expand)AuthorAgeFilesLines
* More rigorous rules for Product type. Propositions and proofs all working, bu...Josh Chen2018-05-291-12/+17
* Dependent product rules done and proofs of typing properties so far work. Sta...Josh Chen2018-05-281-27/+54
* pre-system upgrade commitJosh Chen2018-05-231-35/+40
* Added precedences. Need to figure out how to organize metatypes.Josh Chen2018-05-141-13/+12
* Decided to go with no explicit type declarations in object-lambda expressions...Josh Chen2018-05-101-14/+25
* InitJosh Chen2018-05-031-0/+99