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
(
unfollow
)
Commit message (
Collapse
)
Author
Files
Lines
2020-05-28
bit more material
Josh Chen
1
-10
/
+14
2020-05-28
notation
Josh Chen
1
-0
/
+3
2020-05-28
more List and Maybe
Josh Chen
3
-7
/
+22
2020-05-28
case distinction
Josh Chen
3
-1
/
+68
2020-05-28
reorganize folder structure
Josh Chen
11
-14
/
+14
2020-05-27
change variable name in elim rules and fix small mistake
Josh Chen
3
-23
/
+19
2020-05-27
1. Define Maybe in terms of other types. 2. Move More_Types to Spartan
Josh Chen
2
-28
/
+134
2020-05-26
1. New congruence declarations for calculational reasoning. 2. Remove old ↵
Josh Chen
3
-56
/
+87
elimination tactic.
2020-05-26
Maybe and more List
Josh Chen
2
-7
/
+123
2020-05-25
notation
Josh Chen
1
-0
/
+4
2020-05-25
fix implicits table merge mistake
Josh Chen
1
-1
/
+1
2020-05-25
Lists + more reorganizing
Josh Chen
2
-2
/
+86
2020-05-25
Reorganize theory structure. In particular, the identity type moves out from ↵
Josh Chen
14
-889
/
+15
under Spartan to HoTT. Spartan now only has Pi and Sigma.
2020-05-25
slightly nicer homotopy proofs with calculations
Josh Chen
2
-30
/
+16
2020-05-25
`refl` and `this` methods
Josh Chen
1
-8
/
+20
2020-05-25
use existing calculation infrastructure for sym and trans
Josh Chen
1
-12
/
+3
2020-05-25
1. equality method now uses general elimination tactic. 2. New constant `` ↵
Josh Chen
2
-54
/
+92
refers to rhs of equalities.
2020-05-25
new elimination tactic
Josh Chen
2
-34
/
+68
2020-05-24
new work on elimination tactic
Josh Chen
5
-42
/
+113
2020-05-24
small comment
Josh Chen
1
-0
/
+2
2020-05-22
some tweaks and comments, in preparation for general inductive type elimination
Josh Chen
6
-17
/
+21
2020-04-16
update for Isabelle2020
Josh Chen
2
-2
/
+2
2020-04-02
1. make id function an abbrev. 2. fix reduce method
Josh Chen
2
-8
/
+6
2020-04-02
better lambda notation
Josh Chen
1
-4
/
+7
2020-04-02
Brand-spanking new version using Spartan infrastructure
Josh Chen
13
-0
/
+3068