Commit message (Collapse) | Author | Age | Files | Lines | |
---|---|---|---|---|---|
* | Cleanups and reorganization | Josh Chen | 2019-02-22 | 10 | -397/+153 |
| | |||||
* | Proof of pathcomp associativity done. Some comments | Josh Chen | 2019-02-22 | 3 | -23/+249 |
| | |||||
* | Partway through associativity proof. Lots to work on to make this more usable. | Josh Chen | 2019-02-18 | 1 | -28/+58 |
| | |||||
* | Dependent elimator for Eq now has the correct form. Cleaned up theorems | Josh Chen | 2019-02-17 | 1 | -20/+104 |
| | |||||
* | finalize quantify methods | Josh Chen | 2019-02-17 | 1 | -3/+2 |
| | |||||
* | Method "quantify" converts product inhabitation into Pure universal ↵ | Josh Chen | 2019-02-17 | 6 | -41/+132 |
| | | | | statements. Also misc. cleanups. | ||||
* | Organize this commit as a backup of the work on type inference done so far; ↵ | Josh Chen | 2019-02-11 | 3 | -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 Chen | 2019-02-11 | 4 | -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 Chen | 2019-02-11 | 1 | -3/+23 |
| | |||||
* | restructure library | Josh Chen | 2019-02-10 | 4 | -104/+108 |
| | |||||
* | Fix antiquotation situation | Josh Chen | 2019-02-10 | 1 | -5/+8 |
| | |||||
* | Explicit references in antiquotations in typing.ML. Move trace switch ↵ | Josh Chen | 2019-02-10 | 2 | -6/+6 |
| | | | | definition to HoTT_Base. | ||||
* | Type information storage functionality (assume_type, assume_types keywords) ↵ | Josh Chen | 2019-02-10 | 3 | -64/+237 |
| | | | | done! Inference and pretty-printing for function composition done. | ||||
* | Merge branch '2019': beginning type inference automation. | Josh Chen | 2019-02-05 | 5 | -122/+226 |
|\ | |||||
| * | Add cong named theorem for congruence rules | Josh Chen | 2019-02-05 | 2 | -5/+9 |
| | | |||||
| * | Basic type inference for composed lambda terms! | Josh Chen | 2019-02-05 | 1 | -18/+11 |
| | | |||||
| * | Decided to keep terms eta-expanded | Josh Chen | 2019-02-05 | 1 | -0/+2 |
| | | |||||
| * | Type inference setup begun - first use-case for function composition. | Josh Chen | 2019-02-05 | 3 | -61/+118 |
| | | |||||
| * | 1. Change syntax to rely less on unicode/control symbols. | Josh Chen | 2019-02-04 | 3 | -53/+116 |
| | | | | | | | | 2. Begin work on object-level type inference and input syntax help. | ||||
| * | Text remarks | Josh Chen | 2019-01-31 | 1 | -3/+7 |
| | | |||||
| * | Clean and comment methods file | Josh Chen | 2019-01-30 | 1 | -41/+34 |
| | | |||||
| * | Remove "constrained" notation for type families. Clean and document. | Josh Chen | 2019-01-30 | 1 | -20/+13 |
| | | |||||
| * | Begin refactor | Josh Chen | 2019-01-30 | 1 | -12/+7 |
| | | |||||
* | | Update README.md | Josh Chen | 2018-09-20 | 1 | -1/+1 |
|/ | | | Remove DOI badge | ||||
* | Derive can prove pathcomp_comp. Fix typo. | Josh Chen | 2018-09-20 | 2 | -16/+2 |
| | |||||
* | Application should bind tighter than composition | Josh Chen | 2018-09-20 | 2 | -3/+3 |
| | |||||
* | Rename properties of equality + more properties. Output formatting for ` | Josh Chen | 2018-09-20 | 2 | -1/+216 |
| | |||||
* | Renaming | Josh Chen | 2018-09-19 | 2 | -220/+0 |
| | |||||
* | Renaming | Josh Chen | 2018-09-19 | 3 | -3/+46 |
| | |||||
* | Not sure what advantage is provided by having eta-expanded forms in the ↵ | Josh Chen | 2018-09-19 | 5 | -12/+12 |
| | | | | rules. Removing for now. | ||||
* | proof of associativity of path composition | Josh Chen | 2018-09-19 | 2 | -27/+73 |
| | |||||
* | Merge branch 'larsrh-topic/root' | Josh Chen | 2018-09-18 | 4 | -2/+27 |
|\ | |||||
| * | Add ROOT. No eta-contraction | Josh Chen | 2018-09-18 | 2 | -2/+18 |
| | | |||||
| * | add ROOT file | Lars Hupel | 2018-09-18 | 3 | -2/+11 |
|/ | |||||
* | Load Univalence by default | Josh Chen | 2018-09-18 | 1 | -0/+1 |
| | |||||
* | Update README.md | Josh Chen | 2018-09-18 | 1 | -0/+6 |
| | |||||
* | Update README.md | Josh Chen | 2018-09-18 | 1 | -16/+0 |
| | |||||
* | Merge branch 'develop', ready for release 0.1.0 | Josh Chen | 2018-09-18 | 19 | -1088/+588 |
|\ | |||||
| * | Overhaul of the theory presentations. New methods in HoTT_Methods.thy for ↵ | Josh Chen | 2018-09-18 | 15 | -273/+177 |
| | | | | | | | | handling universes. Commit for release 0.1.0! | ||||
| * | Theories fully reorganized. Well-formedness rules removed. New methods etc. | Josh Chen | 2018-09-18 | 6 | -471/+158 |
| | | |||||
| * | Clean up Equal.thy + some other tweaks | Josh Chen | 2018-09-17 | 3 | -40/+28 |
| | | |||||
| * | Tweak proof | Josh Chen | 2018-09-17 | 2 | -10/+7 |
| | | |||||
| * | Reorganizing theories | Josh Chen | 2018-09-17 | 9 | -219/+155 |
| | | |||||
| * | Moved function composition lemmas into Prod.thy | Josh Chen | 2018-09-17 | 2 | -108/+51 |
| | | |||||
| * | Reorganized HoTT_Base, updated theories | Josh Chen | 2018-09-16 | 16 | -207/+635 |
| |\ | |||||
| * | | begin reorganizing | Josh Chen | 2018-09-15 | 2 | -10/+11 |
| | | | |||||
| * | | Trying to atomize universal quantification | Josh Chen | 2018-08-19 | 1 | -0/+9 |
| | | | |||||
| * | | Higher groupoid structure of types | Josh Chen | 2018-08-19 | 1 | -4/+67 |
| | | | |||||
* | | | Update README.md | Josh Chen | 2018-09-17 | 1 | -3/+1 |
| | | | |||||
* | | | Update README.md | Josh Chen | 2018-09-12 | 1 | -2/+2 |
| | | |