aboutsummaryrefslogtreecommitdiff
path: root/scratch.thy (unfollow)
Commit message (Collapse)AuthorFilesLines
2018-07-03Refactor HoTT_Methods.thy, proved more stuff with new methods.Josh Chen1-18/+2
2018-06-17Decided on a new proper scheme for type rules using the idea of implicit ↵Josh Chen1-0/+24
well-formed contexts and guaranteed conclusion well-formedness. Product type rules now follow this scheme.