aboutsummaryrefslogtreecommitdiff
path: root/mltt/core (follow)
Commit message (Collapse)AuthorAgeFilesLines
* Bad practice huge commit:Josh Chen2021-06-243-60/+94
| | | | | | | 1. Rudimentary prototype definitional package 2. Started univalence 3. Various compatibility fixes and new theory stubs 4. Updated ROOT file
* 1. Put universe level parameters first in automatic term definitions. 2. Add ↵Josh Chen2021-06-234-10/+22
| | | | debugging to typechecker
* Merge branch 'dev'Josh Chen2021-04-171-1/+1
|\
| * Small fix: extraneous variableJosh Chen2021-04-171-1/+1
| |
* | small renameJosh Chen2021-04-101-3/+3
|/
* rename things + some small changesJosh Chen2021-01-3116-0/+3518