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
Commit message (
Expand
)
Author
Age
Files
Lines
...
*
1. Define Maybe in terms of other types. 2. Move More_Types to Spartan
Josh Chen
2020-05-27
2
-30
/
+45
*
move More_Types to Spartan
Josh Chen
2020-05-27
1
-1
/
+1
*
Eckmann-Hilton, first pass
Josh Chen
2020-05-27
3
-3
/
+193
*
new material
Josh Chen
2020-05-26
5
-34
/
+58
*
1. New congruence declarations for calculational reasoning. 2. Remove old eli...
Josh Chen
2020-05-26
3
-56
/
+87
*
Maybe and more List
Josh Chen
2020-05-26
2
-7
/
+123
*
add Maybe
Josh Chen
2020-05-26
1
-0
/
+1
*
more reorganizing
Josh Chen
2020-05-25
5
-15
/
+12
*
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
7
-16
/
+103
*
Reorganize theory structure. In particular, the identity type moves out from ...
Josh Chen
2020-05-25
16
-14
/
+30
*
minor
Josh Chen
2020-05-25
1
-1
/
+1
*
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
*
some arithmetic
Josh Chen
2020-05-25
1
-17
/
+30
*
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 `` re...
Josh Chen
2020-05-25
2
-54
/
+92
*
new elimination tactic
Josh Chen
2020-05-25
2
-34
/
+68
*
new work on elimination tactic
Josh Chen
2020-05-24
6
-43
/
+114
*
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
7
-21
/
+68
*
Update README.md
Josh Chen
2020-04-16
1
-1
/
+1
*
Merge branch 'master' of https://github.com/jaycech3n/Isabelle-HoTT
Josh Chen
2020-04-16
1
-1
/
+1
|
\
|
*
Update README.md
Josh Chen
2020-04-06
1
-2
/
+2
*
|
update for Isabelle2020
Josh Chen
2020-04-16
4
-5
/
+6
*
|
minor naming
Josh Chen
2020-04-16
1
-9
/
+13
|
/
*
1. change var names. 2. add and mul
Josh Chen
2020-04-03
1
-8
/
+11
*
fix ROOT
Josh Chen
2020-04-03
1
-1
/
+1
*
1. Base theory. 2. Fix Nat axioms, addition.
Josh Chen
2020-04-03
2
-11
/
+21
*
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
*
Merge branch 'master' of https://github.com/jaycech3n/Isabelle-HoTT
Josh Chen
2020-04-02
0
-0
/
+0
|
\
|
*
make development shift really obvious
Josh Chen
2020-01-24
1
-2
/
+2
|
*
Update README.md
Josh Chen
2020-01-24
1
-1
/
+1
|
*
Update README.md
Josh Chen
2020-01-24
1
-1
/
+1
|
*
Update README.md
Josh Chen
2020-01-24
1
-3
/
+3
|
*
Change link
Josh Chen
2019-11-29
1
-1
/
+1
|
*
Update README.md
Josh Chen
2019-10-29
1
-3
/
+3
|
*
Update README.md
Josh Chen
2019-10-29
1
-1
/
+2
|
*
Update README.md
Josh Chen
2019-10-29
1
-1
/
+5
|
*
Update README.md
Josh Chen
2019-10-15
1
-0
/
+1
*
|
Brand-spanking new version using Spartan infrastructure
Josh Chen
2020-04-02
35
-1829
/
+3291
|
/
*
More progress. I think we are reaching the limit of what can be conveniently ...
Josh Chen
2019-03-27
2
-24
/
+83
*
working towards biinv_imp_qinv
Josh Chen
2019-03-26
4
-5
/
+202
*
prune import lists
Josh Chen
2019-03-08
3
-153
/
+10
*
type lemmas for derived functions should type the functions themselves
Josh Chen
2019-03-08
2
-29
/
+102
*
some options, renaming
Josh Chen
2019-03-08
3
-2
/
+3
*
Make functions object-level
Josh Chen
2019-03-06
4
-146
/
+173
*
Removed transport section from Eq.thy
Josh Chen
2019-03-03
1
-99
/
+1
[prev]
[next]