aboutsummaryrefslogtreecommitdiff
path: root/scratch.thy (follow)
Commit message (Expand)AuthorAgeFilesLines
* Test theoriesJosh Chen2018-08-181-9/+0
* Rename to distinguish function and path composition; function composition pro...Josh Chen2018-08-151-72/+0
* Well-formation rules are back in the methods; new theory synthesizing the nat...Josh Chen2018-08-141-89/+69
* rcompose doneJosh Chen2018-08-131-33/+16
* Commit before testing polymorphic equality eliminatorJosh Chen2018-08-121-0/+6
* TweaksJosh Chen2018-08-071-0/+6
* Old application syntax incompatible with EisbachJosh Chen2018-08-071-2/+2
* Partway through changing function application syntax style.Josh Chen2018-08-061-98/+94
* Unit and Null types. Methods.Josh Chen2018-07-121-16/+34
* Pre-universe implementation commitJosh Chen2018-07-091-20/+51
* Added attributes to type elimination rules, not sure if these will actually b...Josh Chen2018-07-061-1/+54
* Refactor HoTT_Methods.thy, proved more stuff with new methods.Josh Chen2018-07-031-18/+2
* Decided on a new proper scheme for type rules using the idea of implicit well...Josh Chen2018-06-171-0/+24