aboutsummaryrefslogtreecommitdiff
path: root/HoTT_Methods.thy (follow)
Commit message (Expand)AuthorAgeFilesLines
* Theories fully reorganized. Well-formedness rules removed. New methods etc.Josh Chen2018-09-181-9/+9
* Tweak proofJosh Chen2018-09-171-2/+2
* Reorganizing theoriesJosh Chen2018-09-171-34/+22
* Reorganized HoTT_Base, updated theoriesJosh Chen2018-09-161-3/+3
* Reorganize methodsJosh Chen2018-08-181-19/+23
* Regrouping type rulesJosh Chen2018-08-181-3/+2
* Prod.thy now has the correct definitional equality structure rule. Definition...Josh Chen2018-08-161-1/+1
* Rename to distinguish function and path composition; function composition pro...Josh Chen2018-08-151-1/+1
* Basic compute methodJosh Chen2018-08-151-0/+4
* Tweak proof methods, some type rules; add HoTT Book examplesJosh Chen2018-08-151-7/+7
* Equality inverse and composition done. Cleaned up methods and method example ...Josh Chen2018-08-141-42/+25
* Commit before testing polymorphic equality eliminatorJosh Chen2018-08-121-2/+2
* Rewriting projection functionsJosh Chen2018-08-081-3/+3
* Unit and Null types. Methods.Josh Chen2018-07-121-2/+5
* Universes implemented. Type rules modified accordingly. No more automatic der...Josh Chen2018-07-111-6/+5
* Pre-universe implementation commitJosh Chen2018-07-091-7/+3
* Methods added and organized!Josh Chen2018-07-071-47/+40
* Added attributes to type elimination rules, not sure if these will actually b...Josh Chen2018-07-061-4/+43
* Refactor HoTT_Methods.thy, proved more stuff with new methods.Josh Chen2018-07-031-78/+14
* Rewrote methods: wellformed now two lines, uses named theorems. New, more pow...Josh Chen2018-07-031-57/+86
* EqualityJosh Chen2018-06-301-2/+12
* wellformed method works!!!Josh Chen2018-06-281-6/+6
* wellformed method to automatically prove wellformed judgments derivable from ...Josh Chen2018-06-271-0/+76
generated by cgit v1.2.3 (git 2.25.1) at 2024-12-25 19:52:25 +0000