aboutsummaryrefslogtreecommitdiff
Commit message (Collapse)AuthorAgeFilesLines
* Well-formation rules are back in the methods; new theory synthesizing the ↵Josh Chen2018-08-147-102/+174
| | | | natural number predecessor function.
* Equality inverse and composition done. Cleaned up methods and method example ↵Josh Chen2018-08-145-121/+215
| | | | theory.
* rcompose doneJosh Chen2018-08-137-78/+105
|
* Commit before testing polymorphic equality eliminatorJosh Chen2018-08-129-56/+108
|
* Rewriting projection functionsJosh Chen2018-08-082-211/+7
|
* TweaksJosh Chen2018-08-072-4/+9
|
* Old application syntax incompatible with EisbachJosh Chen2018-08-077-78/+74
|
* Experiment with polymorphic dependent eliminators, i.e. we leave type and ↵Josh Chen2018-08-072-14/+14
| | | | type family decorations implicit.
* Partway through changing function application syntax style.Josh Chen2018-08-067-138/+206
|
* CoproductJosh Chen2018-08-041-0/+61
|
* Reorganize theoriesJosh Chen2018-08-045-100/+130
|
* Unit and Null types. Methods.Josh Chen2018-07-125-19/+73
|
* Universes implemented. Type rules modified accordingly. No more automatic ↵Josh Chen2018-07-117-70/+63
| | | | derivation of "A:U" from "a:A".
* Alternative implementation of universes using meta-level numerals.Josh Chen2018-07-111-32/+43
|
* Pre-universe implementation commitJosh Chen2018-07-096-70/+104
|
* Library snapshot. Methods written, everything nicely organized.Josh Chen2018-07-077-20/+45
|
* Methods added and organized!Josh Chen2018-07-071-47/+40
|
* Remove extra attributes for elimination rules, unneeded for now.Josh Chen2018-07-063-5/+2
|
* Added attributes to type elimination rules, not sure if these will actually ↵Josh Chen2018-07-067-29/+110
| | | | be needed or useful later. Added [comp] attribute to be used by simplification met methods.
* Trivial changesJosh Chen2018-07-042-7/+8
|
* Refactor HoTT_Methods.thy, proved more stuff with new methods.Josh Chen2018-07-039-205/+133
|
* Rewrote methods: wellformed now two lines, uses named theorems. New, more ↵Josh Chen2018-07-036-121/+117
| | | | powerful derive method. Used these to rewrite proofs.
* Proving path composition. Need to set up the Simplifier to simplify ↵Josh Chen2018-06-302-10/+29
| | | | application of object-lambdas to arguments.
* Fix precedence of =Josh Chen2018-06-301-1/+1
|
* EqualityJosh Chen2018-06-303-56/+131
|
* Finished proofs of projectionsJosh Chen2018-06-302-21/+77
|
* Add Pair_introJosh Chen2018-06-301-0/+7
|
* Proving theorems in Proj.thy in a simpler way with wellformedJosh Chen2018-06-281-40/+23
|
* wellformed method works!!!Josh Chen2018-06-281-6/+6
|
* wellformed method to automatically prove wellformed judgments derivable from ↵Josh Chen2018-06-271-0/+76
| | | | a wellformed judgment
* Move projection function definitions out of Sum.thyJosh Chen2018-06-272-170/+197
|
* Library organization and formattingJosh Chen2018-06-274-9/+10
|
* 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-183-23/+95
| | | | 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-183-31/+51
| | | | simplifier. Proved simplification rule for dependent fst.
* Proof of projection functions now harder. Should look up automation methods.Josh Chen2018-06-172-9/+15
|
* Eliminators must be completely parametrized at the meta-level.Josh Chen2018-06-171-14/+5
|
* Decided on a new proper scheme for type rules using the idea of implicit ↵Josh Chen2018-06-173-24/+45
| | | | well-formed contexts and guaranteed conclusion well-formedness. Product type rules now follow this scheme.
* projectionsJosh Chen2018-06-153-40/+44
|
* Type rules now have \"all\" premises explicitly stated, matching the ↵Josh Chen2018-06-126-135/+215
| | | | formulation in the HoTT book.
* Reorganize codeJosh Chen2018-06-096-257/+303
|
* Symmetry and transitivity done.Josh Chen2018-06-072-3/+27
|
* But also looser than PairJosh Chen2018-06-071-1/+1
|
* Nondependent function arrow should bind tighter than the Pi former, but ↵Josh Chen2018-06-072-26/+48
| | | | looser than equality.
* Code formattingJosh Chen2018-06-052-41/+56
|
* Proved that the inductor on Sum has the correct type.Josh Chen2018-06-052-44/+81
|
* Dependent sum done, I think.Josh Chen2018-06-052-28/+42
|
* Prod_comp should have a type constraint. This also fixes a false proof for ↵Josh Chen2018-06-042-36/+69
| | | | the dependent sum projection functions.
* Should be final version of Prod. Theorems proving stuff about currying. ↵Josh Chen2018-06-012-41/+65
| | | | Rules for Sum, going to change them to use object-level arguments more.
* New type rules for dependent product and sum.Josh Chen2018-05-302-21/+33
|
generated by cgit v1.2.3 (git 2.25.1) at 2024-11-03 05:16:56 +0000