Commit message (Collapse) | Author | Age | Files | Lines | ||
---|---|---|---|---|---|---|
... | ||||||
* | more convenient syntax | Josh Chen | 2019-02-28 | 2 | -72/+100 | |
| | ||||||
* | 1. Remove all type inference functionality (feature development moving to ↵ | Josh Chen | 2019-02-28 | 6 | -577/+178 | |
| | | | | | | another branch). 2. Eq.thy complete. | |||||
* | touchups | Josh Chen | 2019-02-23 | 2 | -2/+2 | |
| | ||||||
* | compute method solves subgoals arising from subst | Josh Chen | 2019-02-23 | 1 | -6/+8 | |
| | ||||||
* | readme | Josh Chen | 2019-02-23 | 1 | -3/+12 | |
| | ||||||
* | more proofs involving equality | Josh Chen | 2019-02-23 | 1 | -44/+97 | |
| | ||||||
* | change mixfix pretty-printing indentation | Josh Chen | 2019-02-23 | 2 | -8/+8 | |
| | ||||||
* | rewrite associativity proof | Josh Chen | 2019-02-23 | 1 | -17/+16 | |
| | ||||||
* | 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 | |
| | |