aboutsummaryrefslogtreecommitdiff
path: root/Prod.thy (follow)
Commit message (Collapse)AuthorAgeFilesLines
...
* Removed all [simp] attributes, these will be added later when I set up the ↵Josh Chen2018-06-181-12/+19
| | | | simplifier. Proved simplification rule for dependent fst.
* Decided on a new proper scheme for type rules using the idea of implicit ↵Josh Chen2018-06-171-1/+1
| | | | well-formed contexts and guaranteed conclusion well-formedness. Product type rules now follow this scheme.
* Type rules now have \"all\" premises explicitly stated, matching the ↵Josh Chen2018-06-121-6/+13
| | | | formulation in the HoTT book.
* Reorganize codeJosh Chen2018-06-091-0/+48