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
/
HoTT_Base.thy
(
follow
)
Commit message (
Expand
)
Author
Age
Files
Lines
*
Theories fully reorganized. Well-formedness rules removed. New methods etc.
Josh Chen
2018-09-18
1
-3
/
+1
*
Clean up Equal.thy + some other tweaks
Josh Chen
2018-09-17
1
-1
/
+1
*
Reorganizing theories
Josh Chen
2018-09-17
1
-11
/
+14
*
Reorganized HoTT_Base, updated theories
Josh Chen
2018-09-16
1
-47
/
+40
|
\
|
*
Running into trouble with the polymorphic identity function
Josh Chen
2018-09-11
1
-6
/
+10
|
*
Go back to higher-order application notation
Josh Chen
2018-09-11
1
-8
/
+6
|
*
Some higher groupoid structure proofs
Josh Chen
2018-08-30
1
-1
/
+1
|
*
Should write the correct rule for Ord_leq_min. Another exercise.
Josh Chen
2018-08-30
1
-2
/
+6
|
*
Add leq relation to meta-ordinals, it helps with proofs
Josh Chen
2018-08-30
1
-6
/
+11
*
|
begin reorganizing
Josh Chen
2018-09-15
1
-9
/
+10
|
/
*
Distinguish the typing judgment
Josh Chen
2018-08-18
1
-2
/
+1
*
Regrouping type rules
Josh Chen
2018-08-18
1
-1
/
+0
*
Output formatting
Josh Chen
2018-08-18
1
-1
/
+1
*
Prod.thy now has the correct definitional equality structure rule. Definition...
Josh Chen
2018-08-16
1
-1
/
+1
*
Well-formation rules are back in the methods; new theory synthesizing the nat...
Josh Chen
2018-08-14
1
-1
/
+1
*
Commit before testing polymorphic equality eliminator
Josh Chen
2018-08-12
1
-0
/
+1
*
Old application syntax incompatible with Eisbach
Josh Chen
2018-08-07
1
-4
/
+0
*
Partway through changing function application syntax style.
Josh Chen
2018-08-06
1
-9
/
+12
*
Reorganize theories
Josh Chen
2018-08-04
1
-35
/
+41
*
Unit and Null types. Methods.
Josh Chen
2018-07-12
1
-1
/
+2
*
Universes implemented. Type rules modified accordingly. No more automatic der...
Josh Chen
2018-07-11
1
-23
/
+12
*
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
1
-2
/
+23
*
Library snapshot. Methods written, everything nicely organized.
Josh Chen
2018-07-07
1
-1
/
+1
*
Added attributes to type elimination rules, not sure if these will actually b...
Josh Chen
2018-07-06
1
-3
/
+7
*
Refactor HoTT_Methods.thy, proved more stuff with new methods.
Josh Chen
2018-07-03
1
-1
/
+3
*
Rewrote methods: wellformed now two lines, uses named theorems. New, more pow...
Josh Chen
2018-07-03
1
-4
/
+5
*
Library organization and formatting
Josh Chen
2018-06-27
1
-1
/
+3
*
Fixed wrong definition of snd_dep. Proved projection property of snd_dep. Add...
Josh Chen
2018-06-18
1
-2
/
+1
*
Removed all [simp] attributes, these will be added later when I set up the si...
Josh Chen
2018-06-18
1
-1
/
+1
*
Proof of projection functions now harder. Should look up automation methods.
Josh Chen
2018-06-17
1
-1
/
+1
*
projections
Josh Chen
2018-06-15
1
-27
/
+13
*
Type rules now have \"all\" premises explicitly stated, matching the formulat...
Josh Chen
2018-06-12
1
-15
/
+29
*
Reorganize code
Josh Chen
2018-06-09
1
-0
/
+52