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
(
follow
)
Commit message (
Collapse
)
Author
Age
Files
Lines
*
1. New congruence declarations for calculational reasoning. 2. Remove old ↵
Josh Chen
2020-05-26
3
-56
/
+87
|
|
|
|
elimination tactic.
*
Maybe and more List
Josh Chen
2020-05-26
2
-7
/
+123
|
*
notation
Josh Chen
2020-05-25
1
-0
/
+4
|
*
fix implicits table merge mistake
Josh Chen
2020-05-25
1
-1
/
+1
|
*
Lists + more reorganizing
Josh Chen
2020-05-25
2
-2
/
+86
|
*
Reorganize theory structure. In particular, the identity type moves out from ↵
Josh Chen
2020-05-25
14
-889
/
+15
|
|
|
|
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
2
-34
/
+68
|
*
new work on elimination tactic
Josh Chen
2020-05-24
5
-42
/
+113
|
*
small comment
Josh Chen
2020-05-24
1
-0
/
+2
|
*
some tweaks and comments, in preparation for general inductive type elimination
Josh Chen
2020-05-22
6
-17
/
+21
|
*
update for Isabelle2020
Josh Chen
2020-04-16
2
-2
/
+2
|
*
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
13
-0
/
+3068
