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
(
unfollow
)
Commit message (
Expand
)
Author
Files
Lines
2019-02-10
restructure library
Josh Chen
1
-2
/
+2
2019-02-10
Explicit references in antiquotations in typing.ML. Move trace switch definit...
Josh Chen
1
-0
/
+3
2019-02-10
Type information storage functionality (assume_type, assume_types keywords) d...
Josh Chen
1
-4
/
+34
2019-02-05
Add cong named theorem for congruence rules
Josh Chen
1
-3
/
+6
2019-02-05
Decided to keep terms eta-expanded
Josh Chen
1
-0
/
+2
2019-02-05
Type inference setup begun - first use-case for function composition.
Josh Chen
1
-48
/
+9
2019-02-04
1. Change syntax to rely less on unicode/control symbols.
Josh Chen
1
-12
/
+53
2019-01-31
Text remarks
Josh Chen
1
-3
/
+7
2019-01-30
Remove "constrained" notation for type families. Clean and document.
Josh Chen
1
-20
/
+13
2019-01-30
Begin refactor
Josh Chen
1
-12
/
+7
2018-09-20
Derive can prove pathcomp_comp. Fix typo.
Josh Chen
1
-1
/
+1
2018-09-19
proof of associativity of path composition
Josh Chen
1
-3
/
+8
2018-09-18
Add ROOT. No eta-contraction
Josh Chen
1
-0
/
+2
2018-09-18
Overhaul of the theory presentations. New methods in HoTT_Methods.thy for han...
Josh Chen
1
-14
/
+15
2018-09-18
Theories fully reorganized. Well-formedness rules removed. New methods etc.
Josh Chen
1
-3
/
+1
2018-09-17
Clean up Equal.thy + some other tweaks
Josh Chen
1
-1
/
+1
2018-09-17
Reorganizing theories
Josh Chen
1
-11
/
+14
2018-09-15
begin reorganizing
Josh Chen
1
-9
/
+10
2018-09-11
Running into trouble with the polymorphic identity function
Josh Chen
1
-6
/
+10
2018-09-11
Go back to higher-order application notation
Josh Chen
1
-8
/
+6
2018-08-30
Some higher groupoid structure proofs
Josh Chen
1
-1
/
+1
2018-08-30
Should write the correct rule for Ord_leq_min. Another exercise.
Josh Chen
1
-2
/
+6
2018-08-30
Add leq relation to meta-ordinals, it helps with proofs
Josh Chen
1
-6
/
+11
2018-08-18
Distinguish the typing judgment
Josh Chen
1
-2
/
+1
2018-08-18
Regrouping type rules
Josh Chen
1
-1
/
+0
2018-08-18
Output formatting
Josh Chen
1
-1
/
+1
2018-08-16
Prod.thy now has the correct definitional equality structure rule. Definition...
Josh Chen
1
-1
/
+1
2018-08-16
Prod.thy now has the correct definitional equality structure rule. Definition...
Josh Chen
1
-1
/
+1
2018-08-14
Well-formation rules are back in the methods; new theory synthesizing the nat...
Josh Chen
1
-1
/
+1
2018-08-12
Commit before testing polymorphic equality eliminator
Josh Chen
1
-0
/
+1
2018-08-07
Old application syntax incompatible with Eisbach
Josh Chen
1
-4
/
+0
2018-08-06
Partway through changing function application syntax style.
Josh Chen
1
-9
/
+12
2018-08-04
Reorganize theories
Josh Chen
1
-35
/
+41
2018-07-12
Unit and Null types. Methods.
Josh Chen
1
-1
/
+2
2018-07-11
Universes implemented. Type rules modified accordingly. No more automatic der...
Josh Chen
1
-23
/
+12
2018-07-11
Alternative implementation of universes using meta-level numerals.
Josh Chen
1
-32
/
+43
2018-07-09
Pre-universe implementation commit
Josh Chen
1
-2
/
+23
2018-07-07
Library snapshot. Methods written, everything nicely organized.
Josh Chen
1
-1
/
+1
2018-07-06
Added attributes to type elimination rules, not sure if these will actually b...
Josh Chen
1
-3
/
+7
2018-07-03
Refactor HoTT_Methods.thy, proved more stuff with new methods.
Josh Chen
1
-1
/
+3
2018-07-03
Rewrote methods: wellformed now two lines, uses named theorems. New, more pow...
Josh Chen
1
-4
/
+5
2018-06-27
Library organization and formatting
Josh Chen
1
-1
/
+3
2018-06-18
Fixed wrong definition of snd_dep. Proved projection property of snd_dep. Add...
Josh Chen
1
-2
/
+1
2018-06-18
Removed all [simp] attributes, these will be added later when I set up the si...
Josh Chen
1
-1
/
+1
2018-06-17
Proof of projection functions now harder. Should look up automation methods.
Josh Chen
1
-1
/
+1
2018-06-15
projections
Josh Chen
1
-27
/
+13
2018-06-12
Type rules now have \"all\" premises explicitly stated, matching the formulat...
Josh Chen
1
-15
/
+29
2018-06-09
Reorganize code
Josh Chen
1
-0
/
+52