aboutsummaryrefslogtreecommitdiff
Commit message (Collapse)AuthorAgeFilesLines
* Proof of pathcomp associativity done. Some commentsJosh Chen2019-02-223-23/+249
|
* Partway through associativity proof. Lots to work on to make this more usable.Josh Chen2019-02-181-28/+58
|
* Dependent elimator for Eq now has the correct form. Cleaned up theoremsJosh Chen2019-02-171-20/+104
|
* finalize quantify methodsJosh Chen2019-02-171-3/+2
|
* Method "quantify" converts product inhabitation into Pure universal ↵Josh Chen2019-02-176-41/+132
| | | | statements. Also misc. cleanups.
* Organize this commit as a backup of the work on type inference done so far; ↵Josh Chen2019-02-113-61/+60
| | | | 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.
* Put typing functionality into a .thy and clean up antiquotations, which ↵Josh Chen2019-02-114-109/+125
| | | | results in some reorganization of the theory import structure.
* get_this more robust. Functions to convert ML terms and types to strings.Josh Chen2019-02-111-3/+23
|
* restructure libraryJosh Chen2019-02-104-104/+108
|
* Fix antiquotation situationJosh Chen2019-02-101-5/+8
|
* Explicit references in antiquotations in typing.ML. Move trace switch ↵Josh Chen2019-02-102-6/+6
| | | | definition to HoTT_Base.
* Type information storage functionality (assume_type, assume_types keywords) ↵Josh Chen2019-02-103-64/+237
| | | | done! Inference and pretty-printing for function composition done.
* Merge branch '2019': beginning type inference automation.Josh Chen2019-02-055-122/+226
|\
| * Add cong named theorem for congruence rulesJosh Chen2019-02-052-5/+9
| |
| * Basic type inference for composed lambda terms!Josh Chen2019-02-051-18/+11
| |
| * Decided to keep terms eta-expandedJosh Chen2019-02-051-0/+2
| |
| * Type inference setup begun - first use-case for function composition.Josh Chen2019-02-053-61/+118
| |
| * 1. Change syntax to rely less on unicode/control symbols.Josh Chen2019-02-043-53/+116
| | | | | | | | 2. Begin work on object-level type inference and input syntax help.
| * Text remarksJosh Chen2019-01-311-3/+7
| |
| * Clean and comment methods fileJosh Chen2019-01-301-41/+34
| |
| * Remove "constrained" notation for type families. Clean and document.Josh Chen2019-01-301-20/+13
| |
| * Begin refactorJosh Chen2019-01-301-12/+7
| |
* | Update README.mdJosh Chen2018-09-201-1/+1
|/ | | Remove DOI badge
* Derive can prove pathcomp_comp. Fix typo.Josh Chen2018-09-202-16/+2
|
* Application should bind tighter than compositionJosh Chen2018-09-202-3/+3
|
* Rename properties of equality + more properties. Output formatting for `Josh Chen2018-09-202-1/+216
|
* RenamingJosh Chen2018-09-192-220/+0
|
* RenamingJosh Chen2018-09-193-3/+46
|
* Not sure what advantage is provided by having eta-expanded forms in the ↵Josh Chen2018-09-195-12/+12
| | | | rules. Removing for now.
* proof of associativity of path compositionJosh Chen2018-09-192-27/+73
|
* Merge branch 'larsrh-topic/root'Josh Chen2018-09-184-2/+27
|\
| * Add ROOT. No eta-contractionJosh Chen2018-09-182-2/+18
| |
| * add ROOT fileLars Hupel2018-09-183-2/+11
|/
* Load Univalence by defaultJosh Chen2018-09-181-0/+1
|
* Update README.mdJosh Chen2018-09-181-0/+6
|
* Update README.mdJosh Chen2018-09-181-16/+0
|
* Merge branch 'develop', ready for release 0.1.0Josh Chen2018-09-1819-1088/+588
|\
| * Overhaul of the theory presentations. New methods in HoTT_Methods.thy for ↵Josh Chen2018-09-1815-273/+177
| | | | | | | | handling universes. Commit for release 0.1.0!
| * Theories fully reorganized. Well-formedness rules removed. New methods etc.Josh Chen2018-09-186-471/+158
| |
| * Clean up Equal.thy + some other tweaksJosh Chen2018-09-173-40/+28
| |
| * Tweak proofJosh Chen2018-09-172-10/+7
| |
| * Reorganizing theoriesJosh Chen2018-09-179-219/+155
| |
| * Moved function composition lemmas into Prod.thyJosh Chen2018-09-172-108/+51
| |
| * Reorganized HoTT_Base, updated theoriesJosh Chen2018-09-1616-207/+635
| |\
| * | begin reorganizingJosh Chen2018-09-152-10/+11
| | |
| * | Trying to atomize universal quantificationJosh Chen2018-08-191-0/+9
| | |
| * | Higher groupoid structure of typesJosh Chen2018-08-191-4/+67
| | |
* | | Update README.mdJosh Chen2018-09-171-3/+1
| | |
* | | Update README.mdJosh Chen2018-09-121-2/+2
| | |
* | | Update README.mdJosh Chen2018-09-121-1/+1
| | |
generated by cgit v1.2.3 (git 2.25.1) at 2024-11-03 04:03:29 +0000