aboutsummaryrefslogtreecommitdiff
path: root/Prod.thy (follow)
Commit message (Collapse)AuthorAgeFilesLines
* More progress. I think we are reaching the limit of what can be conveniently ↵Josh Chen2019-03-271-2/+30
| | | | proved with the current implementation.
* working towards biinv_imp_qinvJosh Chen2019-03-261-1/+1
|
* change id precedenceJosh Chen2019-03-011-1/+3
|
* transport and homotopyJosh Chen2019-03-011-1/+1
|
* tweak mixfix prioritiesJosh Chen2019-02-281-5/+14
|
* more convenient syntaxJosh Chen2019-02-281-4/+9
|
* 1. Remove all type inference functionality (feature development moving to ↵Josh Chen2019-02-281-29/+5
| | | | | | another branch). 2. Eq.thy complete.
* change mixfix pretty-printing indentationJosh Chen2019-02-231-5/+5
|
* Cleanups and reorganizationJosh Chen2019-02-221-17/+17
|
* finalize quantify methodsJosh Chen2019-02-171-3/+2
|
* Method "quantify" converts product inhabitation into Pure universal ↵Josh Chen2019-02-171-3/+25
| | | | statements. Also misc. cleanups.
* Organize this commit as a backup of the work on type inference done so far; ↵Josh Chen2019-02-111-12/+12
| | | | 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.
* restructure libraryJosh Chen2019-02-101-1/+1
|
* Fix antiquotation situationJosh Chen2019-02-101-5/+8
|
* Type information storage functionality (assume_type, assume_types keywords) ↵Josh Chen2019-02-101-22/+36
| | | | done! Inference and pretty-printing for function composition done.
* Add cong named theorem for congruence rulesJosh Chen2019-02-051-2/+3
|
* Basic type inference for composed lambda terms!Josh Chen2019-02-051-18/+11
|
* Type inference setup begun - first use-case for function composition.Josh Chen2019-02-051-13/+18
|
* 1. Change syntax to rely less on unicode/control symbols.Josh Chen2019-02-041-40/+61
| | | | 2. Begin work on object-level type inference and input syntax help.
* Application should bind tighter than compositionJosh Chen2018-09-201-1/+1
|
* Rename properties of equality + more properties. Output formatting for `Josh Chen2018-09-201-1/+1
|
* 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!
* Theories fully reorganized. Well-formedness rules removed. New methods etc.Josh Chen2018-09-181-2/+3
|
* Moved function composition lemmas into Prod.thyJosh Chen2018-09-171-51/+51
|
* Reorganized HoTT_Base, updated theoriesJosh Chen2018-09-161-23/+19
|\
| * Implementing univalenceJosh Chen2018-09-111-0/+5
| |
| * Go back to higher-order application notationJosh Chen2018-09-111-11/+11
| |
* | Trying to atomize universal quantificationJosh Chen2018-08-191-0/+9
|/
* Move Empty and Unit types to their own theoriesJosh Chen2018-08-181-19/+0
|
* Reorganize methodsJosh Chen2018-08-181-2/+2
|
* Regrouping type rulesJosh Chen2018-08-181-12/+12
|
* Make function composition a definition instead of an axiomatization (should ↵Josh Chen2018-08-171-9/+1
| | | | not need to worry about preconditions)
* Prod.thy now has the correct definitional equality structure rule. ↵Josh Chen2018-08-161-17/+11
| | | | Definition of function composition and properties.
* Rename to distinguish function and path composition; function composition ↵Josh Chen2018-08-151-8/+18
| | | | proofs, which have issues...
* Basic compute methodJosh Chen2018-08-151-1/+1
|
* Tweak proof methods, some type rules; add HoTT Book examplesJosh Chen2018-08-151-1/+1
|
* Function composition, rename path composition to differentiate the two.Josh Chen2018-08-151-0/+16
|
* rcompose doneJosh Chen2018-08-131-14/+8
|
* Commit before testing polymorphic equality eliminatorJosh Chen2018-08-121-10/+12
|
* Old application syntax incompatible with EisbachJosh Chen2018-08-071-6/+6
|
* Experiment with polymorphic dependent eliminators, i.e. we leave type and ↵Josh Chen2018-08-071-5/+5
| | | | type family decorations implicit.
* Partway through changing function application syntax style.Josh Chen2018-08-061-17/+17
|
* Reorganize theoriesJosh Chen2018-08-041-26/+30
|
* Unit and Null types. Methods.Josh Chen2018-07-121-0/+19
|
* Universes implemented. Type rules modified accordingly. No more automatic ↵Josh Chen2018-07-111-4/+4
| | | | derivation of "A:U" from "a:A".
* Library snapshot. Methods written, everything nicely organized.Josh Chen2018-07-071-0/+1
|
* Remove extra attributes for elimination rules, unneeded for now.Josh Chen2018-07-061-2/+1
|
* 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-1/+1
|
generated by cgit v1.2.3 (git 2.25.1) at 2024-07-03 18:31:22 +0000