aboutsummaryrefslogtreecommitdiff
path: root/HoTT_Typing.thy (follow)
Commit message (Collapse)AuthorAgeFilesLines
* Proof of pathcomp associativity done. Some commentsJosh Chen2019-02-221-1/+1
|
* Put typing functionality into a .thy and clean up antiquotations, which ↵Josh Chen2019-02-111-0/+169
results in some reorganization of the theory import structure.