Isabelle-HoTT - trying to make Isabelle/HoTT work with Isabelle 2021-1

	Commit message (Collapse)	Author	Age	Files	Lines
...
*	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
\|
*	wellformed method to automatically prove wellformed judgments derivable from ↵	Josh Chen	2018-06-27	1	-0/+76
\| \| \| \|	a wellformed judgment
*	Move projection function definitions out of Sum.thy	Josh Chen	2018-06-27	2	-170/+197
\|
*	Library organization and formatting	Josh Chen	2018-06-27	4	-9/+10
\|
*	Dependent projection properties done.	Josh Chen	2018-06-18	1	-27/+58
\|
*	Fixed wrong definition of snd_dep. Proved projection property of snd_dep. ↵	Josh Chen	2018-06-18	3	-23/+95
\| \| \| \|	Added type formation rules expressing necessity of the conditions.
*	Removed all [simp] attributes, these will be added later when I set up the ↵	Josh Chen	2018-06-18	3	-31/+51
\| \| \| \|	simplifier. Proved simplification rule for dependent fst.
*	Proof of projection functions now harder. Should look up automation methods.	Josh Chen	2018-06-17	2	-9/+15
\|
*	Eliminators must be completely parametrized at the meta-level.	Josh Chen	2018-06-17	1	-14/+5
\|
*	Decided on a new proper scheme for type rules using the idea of implicit ↵	Josh Chen	2018-06-17	3	-24/+45
\| \| \| \|	well-formed contexts and guaranteed conclusion well-formedness. Product type rules now follow this scheme.
*	projections	Josh Chen	2018-06-15	3	-40/+44
\|
*	Type rules now have \"all\" premises explicitly stated, matching the ↵	Josh Chen	2018-06-12	6	-135/+215
\| \| \| \|	formulation in the HoTT book.
*	Reorganize code	Josh Chen	2018-06-09	6	-257/+303
\|
*	Symmetry and transitivity done.	Josh Chen	2018-06-07	2	-3/+27
\|
*	But also looser than Pair	Josh Chen	2018-06-07	1	-1/+1
\|
*	Nondependent function arrow should bind tighter than the Pi former, but ↵	Josh Chen	2018-06-07	2	-26/+48
\| \| \| \|	looser than equality.
*	Code formatting	Josh Chen	2018-06-05	2	-41/+56
\|
*	Proved that the inductor on Sum has the correct type.	Josh Chen	2018-06-05	2	-44/+81
\|
*	Dependent sum done, I think.	Josh Chen	2018-06-05	2	-28/+42
\|
*	Prod_comp should have a type constraint. This also fixes a false proof for ↵	Josh Chen	2018-06-04	2	-36/+69
\| \| \| \|	the dependent sum projection functions.
*	Should be final version of Prod. Theorems proving stuff about currying. ↵	Josh Chen	2018-06-01	2	-41/+65
\| \| \| \|	Rules for Sum, going to change them to use object-level arguments more.
*	New type rules for dependent product and sum.	Josh Chen	2018-05-30	2	-21/+33
\|
*	Fixed dependent product rules, hopefully final now.	Josh Chen	2018-05-30	2	-75/+29
\|
*	More rigorous rules for Product type. Propositions and proofs all working, ↵	Josh Chen	2018-05-29	2	-24/+72
\| \| \| \|	but have to think about maybe relaxing the computation rule, or else automating the currying of dependent functions.
*	Dependent product rules done and proofs of typing properties so far work. ↵	Josh Chen	2018-05-28	2	-64/+110
\| \| \| \|	Starting on dependent sums.
*	pre-system upgrade commit	Josh Chen	2018-05-23	3	-93/+108
\|
*	Added precedences. Need to figure out how to organize metatypes.	Josh Chen	2018-05-14	2	-18/+33
\|
*	Decided to go with no explicit type declarations in object-lambda ↵	Josh Chen	2018-05-10	2	-25/+43
\| \| \| \|	expressions. Everything in the proof stuff is working at the moment.
*	Init	Josh Chen	2018-05-03	3	-0/+135