aboutsummaryrefslogtreecommitdiff
path: root/scratch.thy (follow)
Commit message (Expand)AuthorAgeFilesLines
* Unit and Null types. Methods.Josh Chen2018-07-121-16/+34
* Pre-universe implementation commitJosh Chen2018-07-091-20/+51
* Added attributes to type elimination rules, not sure if these will actually b...Josh Chen2018-07-061-1/+54
* Refactor HoTT_Methods.thy, proved more stuff with new methods.Josh Chen2018-07-031-18/+2
* Decided on a new proper scheme for type rules using the idea of implicit well...Josh Chen2018-06-171-0/+24