aboutsummaryrefslogtreecommitdiff
path: root/Sum.thy (follow)
Commit message (Expand)AuthorAgeFilesLines
* Reorganize methodsJosh Chen2018-08-181-1/+1
* Regrouping type rulesJosh Chen2018-08-181-17/+19
* Prod.thy now has the correct definitional equality structure rule. Definition...Josh Chen2018-08-161-1/+1
* rcompose doneJosh Chen2018-08-131-1/+1
* Commit before testing polymorphic equality eliminatorJosh Chen2018-08-121-14/+13
* Old application syntax incompatible with EisbachJosh Chen2018-08-071-14/+14
* Experiment with polymorphic dependent eliminators, i.e. we leave type and typ...Josh Chen2018-08-071-9/+9
* Partway through changing function application syntax style.Josh Chen2018-08-061-7/+9
* Reorganize theoriesJosh Chen2018-08-041-18/+21
* Unit and Null types. Methods.Josh Chen2018-07-121-0/+13
* Universes implemented. Type rules modified accordingly. No more automatic der...Josh Chen2018-07-111-16/+8
* Library snapshot. Methods written, everything nicely organized.Josh Chen2018-07-071-1/+2
* Remove extra attributes for elimination rules, unneeded for now.Josh Chen2018-07-061-1/+0
* Added attributes to type elimination rules, not sure if these will actually b...Josh Chen2018-07-061-0/+2
* Trivial changesJosh Chen2018-07-041-6/+7
* Refactor HoTT_Methods.thy, proved more stuff with new methods.Josh Chen2018-07-031-4/+4
* Rewrote methods: wellformed now two lines, uses named theorems. New, more pow...Josh Chen2018-07-031-1/+1
* Add Pair_introJosh Chen2018-06-301-0/+7
* Move projection function definitions out of Sum.thyJosh Chen2018-06-271-170/+1
* Dependent projection properties done.Josh Chen2018-06-181-27/+58
* Fixed wrong definition of snd_dep. Proved projection property of snd_dep. Add...Josh Chen2018-06-181-16/+81
* Removed all [simp] attributes, these will be added later when I set up the si...Josh Chen2018-06-181-18/+31
* Proof of projection functions now harder. Should look up automation methods.Josh Chen2018-06-171-8/+14
* Eliminators must be completely parametrized at the meta-level.Josh Chen2018-06-171-14/+5
* projectionsJosh Chen2018-06-151-13/+28
* Type rules now have \"all\" premises explicitly stated, matching the formulat...Josh Chen2018-06-121-31/+62
* Reorganize codeJosh Chen2018-06-091-0/+78
generated by cgit v1.2.3 (git 2.25.1) at 2024-12-22 21:44:35 +0000