aboutsummaryrefslogtreecommitdiff
path: root/mltt/core/goals.ML (follow)
Commit message (Collapse)AuthorAgeFilesLines
* 1. Thm/def statement display. 2. Syntax + computation proof.Josh Chen2021-06-281-0/+3
|
* Bad practice huge commit:Josh Chen2021-06-241-35/+66
| | | | | | | 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-231-4/+5
| | | | debugging to typechecker
* rename things + some small changesJosh Chen2021-01-311-0/+213