aboutsummaryrefslogtreecommitdiff
path: root/scratch.thy (unfollow)
Commit message (Expand)AuthorFilesLines
2018-07-12Unit and Null types. Methods.Josh Chen1-16/+34
2018-07-09Pre-universe implementation commitJosh Chen1-20/+51
2018-07-06Added attributes to type elimination rules, not sure if these will actually b...Josh Chen1-1/+54
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 well...Josh Chen1-0/+24