aboutsummaryrefslogtreecommitdiff
path: root/Coprod.thy (unfollow)
Commit message (Collapse)AuthorFilesLines
2019-02-22Cleanups and reorganizationJosh Chen1-50/+0
2018-09-19Not sure what advantage is provided by having eta-expanded forms in the ↵Josh Chen1-3/+3
rules. Removing for now.
2018-09-18Overhaul of the theory presentations. New methods in HoTT_Methods.thy for ↵Josh Chen1-0/+1
handling universes. Commit for release 0.1.0!
2018-09-17Reorganizing theoriesJosh Chen1-40/+24
2018-09-12Some final touchups before release 0.1 for the MS thesisJosh Chen1-1/+1
2018-09-11Go back to higher-order application notationJosh Chen1-17/+17
2018-08-18Reorganize methodsJosh Chen1-1/+1
2018-08-18Regrouping type rulesJosh Chen1-13/+13
2018-08-17Fix silly mistakes in Coprod.thyJosh Chen1-10/+10
2018-08-16Prod.thy now has the correct definitional equality structure rule. ↵Josh Chen1-1/+1
Definition of function composition and properties.
2018-08-16Prod.thy now has the correct definitional equality structure rule. ↵Josh Chen1-1/+1
Definition of function composition and properties.
2018-08-14Well-formation rules are back in the methods; new theory synthesizing the ↵Josh Chen1-5/+9
natural number predecessor function.
2018-08-12Commit before testing polymorphic equality eliminatorJosh Chen1-5/+5
2018-08-07Old application syntax incompatible with EisbachJosh Chen1-20/+20
2018-08-04CoproductJosh Chen1-0/+61
generated by cgit v1.2.3 (git 2.25.1) at 2024-09-06 19:58:04 +0000