aboutsummaryrefslogtreecommitdiff
Commit message (Collapse)AuthorAgeFilesLines
...
* Fixed dependent product rules, hopefully final now.Josh Chen2018-05-302-75/+29
|
* More rigorous rules for Product type. Propositions and proofs all working, ↵Josh Chen2018-05-292-24/+72
| | | | but have to think about maybe relaxing the computation rule, or else automating the currying of dependent functions.
* Dependent product rules done and proofs of typing properties so far work. ↵Josh Chen2018-05-282-64/+110
| | | | Starting on dependent sums.
* pre-system upgrade commitJosh Chen2018-05-233-93/+108
|
* Added precedences. Need to figure out how to organize metatypes.Josh Chen2018-05-142-18/+33
|
* Decided to go with no explicit type declarations in object-lambda ↵Josh Chen2018-05-102-25/+43
| | | | expressions. Everything in the proof stuff is working at the moment.
* InitJosh Chen2018-05-033-0/+135