aboutsummaryrefslogtreecommitdiff
path: root/mltt (unfollow)
Commit message (Collapse)AuthorFilesLines
2021-06-24Bad practice huge commit:Josh Chen6-67/+101
1. Rudimentary prototype definitional package 2. Started univalence 3. Various compatibility fixes and new theory stubs 4. Updated ROOT file
2021-06-231. Put universe level parameters first in automatic term definitions. 2. Add ↵Josh Chen4-10/+22
debugging to typechecker
2021-04-17Small fix: extraneous variableJosh Chen1-1/+1
2021-04-10small renameJosh Chen1-3/+3
2021-01-31rename things + some small changesJosh Chen19-0/+3937