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
*
Update README.md
Josh Chen
2018-08-17
1
-1
/
+6
*
Add contact
Josh Chen
2018-08-17
1
-1
/
+1
*
Update README.md
Josh Chen
2018-08-17
1
-1
/
+1
*
Update README.md
Josh Chen
2018-08-17
1
-1
/
+2
*
Create README.md
Josh Chen
2018-08-17
1
-0
/
+16
*
Remove test commit folder
Josh Chen
2018-08-17
1
-1
/
+0
*
Partway through updating proofs after the change of the function composition ...
Josh Chen
2018-08-17
1
-46
/
+11
*
Axiomatizations should be definitions
Josh Chen
2018-08-17
1
-4
/
+2
*
Make function composition a definition instead of an axiomatization (should n...
Josh Chen
2018-08-17
1
-9
/
+1
*
Change unnecessary axiomatization to a definition
Josh Chen
2018-08-17
1
-2
/
+2
*
Testing with the new theory
Josh Chen
2018-08-17
1
-29
/
+25
*
second test
Josh Chen
2018-08-16
1
-0
/
+1
*
test new machine
Josh Chen
2018-08-16
1
-0
/
+2
*
Some comments and reorganization
Josh Chen
2018-08-16
2
-24
/
+42
*
Merge branch 'master' of github.com:jaycech3n/HoTT
Josh Chen
2018-08-16
0
-0
/
+0
|
\
|
*
Prod.thy now has the correct definitional equality structure rule. Definition...
Josh Chen
2018-08-16
13
-59
/
+105
*
|
Prod.thy now has the correct definitional equality structure rule. Definition...
Josh Chen
2018-08-16
13
-59
/
+105
|
/
*
Rename to distinguish function and path composition; function composition pro...
Josh Chen
2018-08-15
5
-101
/
+93
*
Basic compute method
Josh Chen
2018-08-15
5
-12
/
+45
*
Tweak proof methods, some type rules; add HoTT Book examples
Josh Chen
2018-08-15
7
-50
/
+87
*
Function composition, rename path composition to differentiate the two.
Josh Chen
2018-08-15
2
-20
/
+36
*
Well-formation rules are back in the methods; new theory synthesizing the nat...
Josh Chen
2018-08-14
7
-102
/
+174
*
Equality inverse and composition done. Cleaned up methods and method example ...
Josh Chen
2018-08-14
5
-121
/
+215
*
rcompose done
Josh Chen
2018-08-13
7
-78
/
+105
*
Commit before testing polymorphic equality eliminator
Josh Chen
2018-08-12
9
-56
/
+108
*
Rewriting projection functions
Josh Chen
2018-08-08
2
-211
/
+7
*
Tweaks
Josh Chen
2018-08-07
2
-4
/
+9
*
Old application syntax incompatible with Eisbach
Josh Chen
2018-08-07
7
-78
/
+74
*
Experiment with polymorphic dependent eliminators, i.e. we leave type and typ...
Josh Chen
2018-08-07
2
-14
/
+14
*
Partway through changing function application syntax style.
Josh Chen
2018-08-06
7
-138
/
+206
*
Coproduct
Josh Chen
2018-08-04
1
-0
/
+61
*
Reorganize theories
Josh Chen
2018-08-04
5
-100
/
+130
*
Unit and Null types. Methods.
Josh Chen
2018-07-12
5
-19
/
+73
*
Universes implemented. Type rules modified accordingly. No more automatic der...
Josh Chen
2018-07-11
7
-70
/
+63
*
Alternative implementation of universes using meta-level numerals.
Josh Chen
2018-07-11
1
-32
/
+43
*
Pre-universe implementation commit
Josh Chen
2018-07-09
6
-70
/
+104
*
Library snapshot. Methods written, everything nicely organized.
Josh Chen
2018-07-07
7
-20
/
+45
*
Methods added and organized!
Josh Chen
2018-07-07
1
-47
/
+40
*
Remove extra attributes for elimination rules, unneeded for now.
Josh Chen
2018-07-06
3
-5
/
+2
*
Added attributes to type elimination rules, not sure if these will actually b...
Josh Chen
2018-07-06
7
-29
/
+110
*
Trivial changes
Josh Chen
2018-07-04
2
-7
/
+8
*
Refactor HoTT_Methods.thy, proved more stuff with new methods.
Josh Chen
2018-07-03
9
-205
/
+133
*
Rewrote methods: wellformed now two lines, uses named theorems. New, more pow...
Josh Chen
2018-07-03
6
-121
/
+117
*
Proving path composition. Need to set up the Simplifier to simplify applicati...
Josh Chen
2018-06-30
2
-10
/
+29
*
Fix precedence of =
Josh Chen
2018-06-30
1
-1
/
+1
*
Equality
Josh Chen
2018-06-30
3
-56
/
+131
*
Finished proofs of projections
Josh Chen
2018-06-30
2
-21
/
+77
*
Add Pair_intro
Josh Chen
2018-06-30
1
-0
/
+7
*
Proving theorems in Proj.thy in a simpler way with wellformed
Josh Chen
2018-06-28
1
-40
/
+23
*
wellformed method works!!!
Josh Chen
2018-06-28
1
-6
/
+6
[next]