aboutsummaryrefslogtreecommitdiff
Commit message (Collapse)AuthorAgeFilesLines
...
* Proved that the inductor on Sum has the correct type.Josh Chen2018-06-052-44/+81
|
* Dependent sum done, I think.Josh Chen2018-06-052-28/+42
|
* Prod_comp should have a type constraint. This also fixes a false proof for ↵Josh Chen2018-06-042-36/+69
| | | | the dependent sum projection functions.
* Should be final version of Prod. Theorems proving stuff about currying. ↵Josh Chen2018-06-012-41/+65
| | | | Rules for Sum, going to change them to use object-level arguments more.
* New type rules for dependent product and sum.Josh Chen2018-05-302-21/+33
|
* 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