aboutsummaryrefslogtreecommitdiff
path: root/hott/List_HoTT.thy (follow)
Commit message (Collapse)AuthorAgeFilesLines
* 1. Thm/def statement display. 2. Syntax + computation proof.Josh Chen2021-06-281-2/+2
|
* Bad practice huge commit:Josh Chen2021-06-241-2/+2
| | | | | | | 1. Rudimentary prototype definitional package 2. Started univalence 3. Various compatibility fixes and new theory stubs 4. Updated ROOT file
* rename things + some small changesJosh Chen2021-01-311-1/+1
|
* Swapped notation for metas (now ?) and holes (now {}), other notation and ↵Josh Chen2021-01-181-0/+18
name changes.