index
:
Isabelle-HoTT
master
trying to make Isabelle/HoTT work with Isabelle 2021-1
about
summary
refs
log
tree
commit
diff
log msg
author
committer
range
path:
root
/
HoTT.thy
(
follow
)
Commit message (
Expand
)
Author
Age
Files
Lines
*
Proved that the inductor on Sum has the correct type.
Josh Chen
2018-06-05
1
-17
/
+31
*
Dependent sum done, I think.
Josh Chen
2018-06-05
1
-28
/
+40
*
Prod_comp should have a type constraint. This also fixes a false proof for th...
Josh Chen
2018-06-04
1
-22
/
+31
*
Should be final version of Prod. Theorems proving stuff about currying. Rules...
Josh Chen
2018-06-01
1
-22
/
+15
*
New type rules for dependent product and sum.
Josh Chen
2018-05-30
1
-12
/
+29
*
Fixed dependent product rules, hopefully final now.
Josh Chen
2018-05-30
1
-3
/
+2
*
More rigorous rules for Product type. Propositions and proofs all working, bu...
Josh Chen
2018-05-29
1
-12
/
+17
*
Dependent product rules done and proofs of typing properties so far work. Sta...
Josh Chen
2018-05-28
1
-27
/
+54
*
pre-system upgrade commit
Josh Chen
2018-05-23
1
-35
/
+40
*
Added precedences. Need to figure out how to organize metatypes.
Josh Chen
2018-05-14
1
-13
/
+12
*
Decided to go with no explicit type declarations in object-lambda expressions...
Josh Chen
2018-05-10
1
-14
/
+25
*
Init
Josh Chen
2018-05-03
1
-0
/
+99