aboutsummaryrefslogtreecommitdiff
path: root/hott/More_List.thy (follow)
Commit message (Collapse)AuthorAgeFilesLines
* 1. Type-checking/inference now more principled, and the implementation is ↵Josh Chen2020-07-211-2/+2
| | | | better. 2. Changed most tactics to context tactics.
* Non-annotated object lambdaJosh Chen2020-07-091-1/+1
|
* proved a few oopses + minor tweaksJosh Chen2020-05-291-11/+1
|
* minorJosh Chen2020-05-291-1/+1
|
* new materialJosh Chen2020-05-261-1/+21
|
* more reorganizingJosh Chen2020-05-251-0/+8