Commit message (Collapse) | Author | Age | Files | Lines | |
---|---|---|---|---|---|
* | Update README.md | Josh Chen | 2019-10-29 | 1 | -1/+2 |
| | |||||
* | Update README.md | Josh Chen | 2019-10-29 | 1 | -1/+5 |
| | |||||
* | Update README.md | Josh Chen | 2019-10-15 | 1 | -0/+1 |
| | |||||
* | More progress. I think we are reaching the limit of what can be conveniently ↵ | Josh Chen | 2019-03-27 | 2 | -24/+83 |
| | | | | proved with the current implementation. | ||||
* | working towards biinv_imp_qinv | Josh Chen | 2019-03-26 | 4 | -5/+202 |
| | |||||
* | prune import lists | Josh Chen | 2019-03-08 | 3 | -153/+10 |
| | |||||
* | type lemmas for derived functions should type the functions themselves | Josh Chen | 2019-03-08 | 2 | -29/+102 |
| | |||||
* | some options, renaming | Josh Chen | 2019-03-08 | 3 | -2/+3 |
| | |||||
* | Make functions object-level | Josh Chen | 2019-03-06 | 4 | -146/+173 |
| | |||||
* | Removed transport section from Eq.thy | Josh Chen | 2019-03-03 | 1 | -99/+1 |
| | |||||
* | Move definition of transport to Type_Families.thy, and change it to use ↵ | Josh Chen | 2019-03-03 | 2 | -79/+147 |
| | | | | meta-functions for type families again. This together with the previous commit simplifies the definitions and proofs for idtoeqv greatly. | ||||
* | Improve automated handling of universes. derive now can automatically handle ↵ | Josh Chen | 2019-03-03 | 2 | -2/+13 |
| | | | | more proofs requiring the use of "U i: U (Suc i)", and shouldn't loop as much. | ||||
* | Defined idtoeqv. Should next state univalence in terms of an explicit ↵ | Josh Chen | 2019-03-03 | 1 | -13/+50 |
| | | | | inverse equivalence. | ||||
* | finished proof of transport_biinv | Josh Chen | 2019-03-01 | 2 | -17/+21 |
| | |||||
* | Proving transport is bi-invertible is harder than expected | Josh Chen | 2019-03-01 | 1 | -83/+87 |
| | |||||
* | change id precedence | Josh Chen | 2019-03-01 | 2 | -14/+16 |
| | |||||
* | transport and homotopy | Josh Chen | 2019-03-01 | 2 | -22/+81 |
| | |||||
* | Working on univalence | Josh Chen | 2019-03-01 | 1 | -46/+115 |
| | |||||
* | Syntax changes. Transport inverse lemmas. | Josh Chen | 2019-03-01 | 1 | -18/+70 |
| | |||||
* | tweak mixfix priorities | Josh Chen | 2019-02-28 | 2 | -7/+16 |
| | |||||
* | 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 |
| | |