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
...
*
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
*
Move definition of transport to Type_Families.thy, and change it to use meta-...
Josh Chen
2019-03-03
2
-79
/
+147
*
Improve automated handling of universes. derive now can automatically handle ...
Josh Chen
2019-03-03
2
-2
/
+13
*
Defined idtoeqv. Should next state univalence in terms of an explicit inverse...
Josh Chen
2019-03-03
1
-13
/
+50
*
finished proof of transport_biinv
Josh Chen
2019-03-01
2
-17
/
+21
*
Proving transport is bi-invertible is harder than expected
Josh Chen
2019-03-01
1
-83
/
+87
*
change id precedence
Josh Chen
2019-03-01
2
-14
/
+16
*
transport and homotopy
Josh Chen
2019-03-01
2
-22
/
+81
*
Working on univalence
Josh Chen
2019-03-01
1
-46
/
+115
*
Syntax changes. Transport inverse lemmas.
Josh Chen
2019-03-01
1
-18
/
+70
*
tweak mixfix priorities
Josh Chen
2019-02-28
2
-7
/
+16
*
more convenient syntax
Josh Chen
2019-02-28
2
-72
/
+100
*
1. Remove all type inference functionality (feature development moving to ano...
Josh Chen
2019-02-28
6
-577
/
+178
*
touchups
Josh Chen
2019-02-23
2
-2
/
+2
*
compute method solves subgoals arising from subst
Josh Chen
2019-02-23
1
-6
/
+8
*
readme
Josh Chen
2019-02-23
1
-3
/
+12
*
more proofs involving equality
Josh Chen
2019-02-23
1
-44
/
+97
*
change mixfix pretty-printing indentation
Josh Chen
2019-02-23
2
-8
/
+8
*
rewrite associativity proof
Josh Chen
2019-02-23
1
-17
/
+16
*
Cleanups and reorganization
Josh Chen
2019-02-22
10
-397
/
+153
*
Proof of pathcomp associativity done. Some comments
Josh Chen
2019-02-22
3
-23
/
+249
*
Partway through associativity proof. Lots to work on to make this more usable.
Josh Chen
2019-02-18
1
-28
/
+58
*
Dependent elimator for Eq now has the correct form. Cleaned up theorems
Josh Chen
2019-02-17
1
-20
/
+104
*
finalize quantify methods
Josh Chen
2019-02-17
1
-3
/
+2
*
Method "quantify" converts product inhabitation into Pure universal statement...
Josh Chen
2019-02-17
6
-41
/
+132
*
Organize this commit as a backup of the work on type inference done so far; l...
Josh Chen
2019-02-11
3
-61
/
+60
*
Put typing functionality into a .thy and clean up antiquotations, which resul...
Josh Chen
2019-02-11
4
-109
/
+125
*
get_this more robust. Functions to convert ML terms and types to strings.
Josh Chen
2019-02-11
1
-3
/
+23
*
restructure library
Josh Chen
2019-02-10
4
-104
/
+108
*
Fix antiquotation situation
Josh Chen
2019-02-10
1
-5
/
+8
*
Explicit references in antiquotations in typing.ML. Move trace switch definit...
Josh Chen
2019-02-10
2
-6
/
+6
*
Type information storage functionality (assume_type, assume_types keywords) d...
Josh Chen
2019-02-10
3
-64
/
+237
*
Merge branch '2019': beginning type inference automation.
Josh Chen
2019-02-05
5
-122
/
+226
|
\
|
*
Add cong named theorem for congruence rules
Josh Chen
2019-02-05
2
-5
/
+9
|
*
Basic type inference for composed lambda terms!
Josh Chen
2019-02-05
1
-18
/
+11
|
*
Decided to keep terms eta-expanded
Josh Chen
2019-02-05
1
-0
/
+2
|
*
Type inference setup begun - first use-case for function composition.
Josh Chen
2019-02-05
3
-61
/
+118
|
*
1. Change syntax to rely less on unicode/control symbols.
Josh Chen
2019-02-04
3
-53
/
+116
|
*
Text remarks
Josh Chen
2019-01-31
1
-3
/
+7
|
*
Clean and comment methods file
Josh Chen
2019-01-30
1
-41
/
+34
|
*
Remove "constrained" notation for type families. Clean and document.
Josh Chen
2019-01-30
1
-20
/
+13
|
*
Begin refactor
Josh Chen
2019-01-30
1
-12
/
+7
*
|
Update README.md
Josh Chen
2018-09-20
1
-1
/
+1
|
/
*
Derive can prove pathcomp_comp. Fix typo.
Josh Chen
2018-09-20
2
-16
/
+2
*
Application should bind tighter than composition
Josh Chen
2018-09-20
2
-3
/
+3
*
Rename properties of equality + more properties. Output formatting for `
Josh Chen
2018-09-20
2
-1
/
+216
*
Renaming
Josh Chen
2018-09-19
2
-220
/
+0
*
Renaming
Josh Chen
2018-09-19
3
-3
/
+46
*
Not sure what advantage is provided by having eta-expanded forms in the rules...
Josh Chen
2018-09-19
5
-12
/
+12
[prev]
[next]