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
/
spartan
/
theories
(
follow
)
Commit message (
Collapse
)
Author
Age
Files
Lines
*
Reorganize theory structure. In particular, the identity type moves out from ↵
Josh Chen
2020-05-25
3
-1361
/
+0
|
|
|
|
under Spartan to HoTT. Spartan now only has Pi and Sigma.
*
slightly nicer homotopy proofs with calculations
Josh Chen
2020-05-25
2
-30
/
+16
|
*
`refl` and `this` methods
Josh Chen
2020-05-25
1
-8
/
+20
|
*
use existing calculation infrastructure for sym and trans
Josh Chen
2020-05-25
1
-12
/
+3
|
*
1. equality method now uses general elimination tactic. 2. New constant `` ↵
Josh Chen
2020-05-25
2
-54
/
+92
|
|
|
|
refers to rhs of equalities.
*
new elimination tactic
Josh Chen
2020-05-25
1
-17
/
+3
|
*
new work on elimination tactic
Josh Chen
2020-05-24
3
-8
/
+28
|
*
some tweaks and comments, in preparation for general inductive type elimination
Josh Chen
2020-05-22
3
-14
/
+14
|
*
1. make id function an abbrev. 2. fix reduce method
Josh Chen
2020-04-02
2
-8
/
+6
|
*
better lambda notation
Josh Chen
2020-04-02
1
-4
/
+7
|
*
Brand-spanking new version using Spartan infrastructure
Josh Chen
2020-04-02
3
-0
/
+1327