aboutsummaryrefslogtreecommitdiff
path: root/Sum.thy (follow)
Commit message (Collapse)AuthorAgeFilesLines
* change mixfix pretty-printing indentationJosh Chen2019-02-231-3/+3
|
* Method "quantify" converts product inhabitation into Pure universal ↵Josh Chen2019-02-171-2/+2
| | | | statements. Also misc. cleanups.
* Organize this commit as a backup of the work on type inference done so far; ↵Josh Chen2019-02-111-27/+24
| | | | learnt that I probably need to take a different approach. In particular, should first make the constants completely monomorphic, and then work on full proper type inference, rather than the heuristic approach taken here.
* Not sure what advantage is provided by having eta-expanded forms in the ↵Josh Chen2018-09-191-2/+2
| | | | rules. Removing for now.
* Overhaul of the theory presentations. New methods in HoTT_Methods.thy for ↵Josh Chen2018-09-181-0/+1
| | | | handling universes. Commit for release 0.1.0!
* Reorganizing theoriesJosh Chen2018-09-171-34/+23
|
* Reorganized HoTT_Base, updated theoriesJosh Chen2018-09-161-19/+19
|\
| * Some final touchups before release 0.1 for the MS thesisJosh Chen2018-09-121-1/+1
| |
| * Go back to higher-order application notationJosh Chen2018-09-111-12/+12
|/
* Move Empty and Unit types to their own theoriesJosh Chen2018-08-181-13/+0
|
* 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. ↵Josh Chen2018-08-161-1/+1
| | | | Definition of function composition and properties.
* 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 ↵Josh Chen2018-08-071-9/+9
| | | | type family decorations implicit.
* 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 ↵Josh Chen2018-07-111-16/+8
| | | | derivation of "A:U" from "a:A".
* 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 ↵Josh Chen2018-07-061-0/+2
| | | | be needed or useful later. Added [comp] attribute to be used by simplification met methods.
* 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 ↵Josh Chen2018-07-031-1/+1
| | | | powerful derive method. Used these to rewrite proofs.
* 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. ↵Josh Chen2018-06-181-16/+81
| | | | Added type formation rules expressing necessity of the conditions.
* Removed all [simp] attributes, these will be added later when I set up the ↵Josh Chen2018-06-181-18/+31
| | | | simplifier. Proved simplification rule for dependent fst.
* 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 ↵Josh Chen2018-06-121-31/+62
| | | | formulation in the HoTT book.
* Reorganize codeJosh Chen2018-06-091-0/+78
generated by cgit v1.2.3 (git 2.25.1) at 2024-11-18 08:03:41 +0000