aboutsummaryrefslogtreecommitdiff
path: root/Equal.thy (follow)
Commit message (Expand)AuthorAgeFilesLines
* Fixed mistake in Equal_elim and proof of rpathcomp_compJosh Chen2018-08-181-1/+1
* Prod.thy now has the correct definitional equality structure rule. Definition...Josh Chen2018-08-161-1/+1
* Well-formation rules are back in the methods; new theory synthesizing the nat...Josh Chen2018-08-141-3/+7
* rcompose doneJosh Chen2018-08-131-6/+6
* Commit before testing polymorphic equality eliminatorJosh Chen2018-08-121-10/+10
* Old application syntax incompatible with EisbachJosh Chen2018-08-071-17/+17
* Reorganize theoriesJosh Chen2018-08-041-13/+16
* Universes implemented. Type rules modified accordingly. No more automatic der...Josh Chen2018-07-111-8/+8
* Library snapshot. Methods written, everything nicely organized.Josh Chen2018-07-071-0/+1
* Remove extra attributes for elimination rules, unneeded for now.Josh Chen2018-07-061-2/+1
* Added attributes to type elimination rules, not sure if these will actually b...Josh Chen2018-07-061-0/+2
* Refactor HoTT_Methods.thy, proved more stuff with new methods.Josh Chen2018-07-031-1/+1
* Fix precedence of =Josh Chen2018-06-301-1/+1
* EqualityJosh Chen2018-06-301-54/+29
* Library organization and formattingJosh Chen2018-06-271-1/+0
* Type rules now have \"all\" premises explicitly stated, matching the formulat...Josh Chen2018-06-121-75/+79
* Reorganize codeJosh Chen2018-06-091-0/+81
generated by cgit v1.2.3 (git 2.25.1) at 2024-12-22 20:27:40 +0000