| Commit message (Expand) | Author | Age | Files | Lines |
* | rename things + some small changes | Josh Chen | 2021-01-31 | 1 | -2/+2 |
* | renamings | Josh Chen | 2021-01-21 | 1 | -33/+25 |
* | Swapped notation for metas (now ?) and holes (now {}), other notation and nam... | Josh Chen | 2021-01-18 | 1 | -14/+21 |
* | Basic experiments adding reduction to the type checker | Josh Chen | 2020-09-23 | 1 | -42/+6 |
* | (FEAT) Context data slots for known types and conditional type rules, as well... | Josh Chen | 2020-08-14 | 1 | -19/+15 |
* | (FEAT) Clean up typechecking/elaboration tactic: known_ctac should *solve* go... | Josh Chen | 2020-08-09 | 1 | -7/+6 |
* | 1. fix intros method. 2. Couple extra lemmas; good small test cases for norma... | Josh Chen | 2020-08-05 | 1 | -1/+20 |
* | (FEAT) SIDE_CONDS tactical has additional argument specifying how many initia... | Josh Chen | 2020-08-03 | 1 | -14/+6 |
* | rename some theorems | Josh Chen | 2020-08-02 | 1 | -9/+9 |
* | (REF) Tweak attribute names in preparation for new logical introduction rule ... | Josh Chen | 2020-07-31 | 1 | -16/+16 |
* | (FEAT) Term elaboration of assumption and goal statements. | Josh Chen | 2020-07-31 | 1 | -207/+249 |
* | Hook elaboration into assumptions mechanism | Josh Chen | 2020-07-27 | 1 | -10/+13 |
* | 1. Bugfix: implicits now properly name schematic variables. Fixes problems ca... | Josh Chen | 2020-07-21 | 1 | -12/+12 |
* | 1. Type-checking/inference now more principled, and the implementation is bet... | Josh Chen | 2020-07-21 | 1 | -26/+26 |
* | Non-annotated object lambda | Josh Chen | 2020-07-09 | 1 | -6/+6 |
* | rule name | Josh Chen | 2020-06-03 | 1 | -1/+1 |
* | proved a few oopses + minor tweaks | Josh Chen | 2020-05-29 | 1 | -19/+22 |
* | clean up Eckmann-Hilton and move to Identity | Josh Chen | 2020-05-29 | 1 | -21/+25 |
* | new material | Josh Chen | 2020-05-26 | 1 | -7/+8 |
* | Reorganize theory structure. In particular, the identity type moves out from ... | Josh Chen | 2020-05-25 | 1 | -0/+416 |