aboutsummaryrefslogtreecommitdiff
path: root/HoTT_Test.thy (unfollow)
Commit message (Expand)AuthorFilesLines
2018-08-17Testing with the new theoryJosh Chen1-29/+25
2018-08-16test new machineJosh Chen1-0/+2
2018-08-16Some comments and reorganizationJosh Chen1-24/+35
2018-08-16Prod.thy now has the correct definitional equality structure rule. Definition...Josh Chen1-1/+1
2018-08-16Prod.thy now has the correct definitional equality structure rule. Definition...Josh Chen1-1/+1
2018-06-27Library organization and formattingJosh Chen1-1/+0
2018-06-17Decided on a new proper scheme for type rules using the idea of implicit well...Josh Chen1-23/+20
2018-06-15projectionsJosh Chen1-0/+3
2018-06-12Type rules now have \"all\" premises explicitly stated, matching the formulat...Josh Chen1-8/+17
2018-06-09Reorganize codeJosh Chen1-9/+44
2018-06-07Symmetry and transitivity done.Josh Chen1-0/+1
2018-06-07Nondependent function arrow should bind tighter than the Pi former, but loose...Josh Chen1-5/+5
2018-06-05Code formattingJosh Chen1-0/+2
2018-06-05Proved that the inductor on Sum has the correct type.Josh Chen1-27/+50
2018-06-05Dependent sum done, I think.Josh Chen1-0/+2
2018-06-04Prod_comp should have a type constraint. This also fixes a false proof for th...Josh Chen1-14/+38
2018-06-01Should be final version of Prod. Theorems proving stuff about currying. Rules...Josh Chen1-19/+50
2018-05-30New type rules for dependent product and sum.Josh Chen1-9/+4
2018-05-30Fixed dependent product rules, hopefully final now.Josh Chen1-72/+27
2018-05-29More rigorous rules for Product type. Propositions and proofs all working, bu...Josh Chen1-12/+55
2018-05-28Dependent product rules done and proofs of typing properties so far work. Sta...Josh Chen1-37/+56
2018-05-23pre-system upgrade commitJosh Chen1-0/+68
generated by cgit v1.2.3 (git 2.25.1) at 2024-11-17 16:53:59 +0000