aboutsummaryrefslogtreecommitdiff
path: root/HoTT_Base.thy (follow)
Commit message (Expand)AuthorAgeFilesLines
* some options, renamingJosh Chen2019-03-081-0/+1
* Improve automated handling of universes. derive now can automatically handle ...Josh Chen2019-03-031-0/+10
* tweak mixfix prioritiesJosh Chen2019-02-281-2/+2
* 1. Remove all type inference functionality (feature development moving to ano...Josh Chen2019-02-281-1/+10
* Method "quantify" converts product inhabitation into Pure universal statement...Josh Chen2019-02-171-5/+8
* Put typing functionality into a .thy and clean up antiquotations, which resul...Josh Chen2019-02-111-47/+6
* restructure libraryJosh Chen2019-02-101-2/+2
* Explicit references in antiquotations in typing.ML. Move trace switch definit...Josh Chen2019-02-101-0/+3
* Type information storage functionality (assume_type, assume_types keywords) d...Josh Chen2019-02-101-4/+34
* Add cong named theorem for congruence rulesJosh Chen2019-02-051-3/+6
* Decided to keep terms eta-expandedJosh Chen2019-02-051-0/+2
* Type inference setup begun - first use-case for function composition.Josh Chen2019-02-051-48/+9
* 1. Change syntax to rely less on unicode/control symbols.Josh Chen2019-02-041-12/+53
* Text remarksJosh Chen2019-01-311-3/+7
* Remove "constrained" notation for type families. Clean and document.Josh Chen2019-01-301-20/+13
* Begin refactorJosh Chen2019-01-301-12/+7
* Derive can prove pathcomp_comp. Fix typo.Josh Chen2018-09-201-1/+1
* proof of associativity of path compositionJosh Chen2018-09-191-3/+8
* Add ROOT. No eta-contractionJosh Chen2018-09-181-0/+2
* Overhaul of the theory presentations. New methods in HoTT_Methods.thy for han...Josh Chen2018-09-181-14/+15
* Theories fully reorganized. Well-formedness rules removed. New methods etc.Josh Chen2018-09-181-3/+1
* Clean up Equal.thy + some other tweaksJosh Chen2018-09-171-1/+1
* Reorganizing theoriesJosh Chen2018-09-171-11/+14
* Reorganized HoTT_Base, updated theoriesJosh Chen2018-09-161-47/+40
|\
| * Running into trouble with the polymorphic identity functionJosh Chen2018-09-111-6/+10
| * Go back to higher-order application notationJosh Chen2018-09-111-8/+6
| * Some higher groupoid structure proofsJosh Chen2018-08-301-1/+1
| * Should write the correct rule for Ord_leq_min. Another exercise.Josh Chen2018-08-301-2/+6
| * Add leq relation to meta-ordinals, it helps with proofsJosh Chen2018-08-301-6/+11
* | begin reorganizingJosh Chen2018-09-151-9/+10
|/
* Distinguish the typing judgmentJosh Chen2018-08-181-2/+1
* Regrouping type rulesJosh Chen2018-08-181-1/+0
* Output formattingJosh Chen2018-08-181-1/+1
* Prod.thy now has the correct definitional equality structure rule. Definition...Josh Chen2018-08-161-1/+1
* Well-formation rules are back in the methods; new theory synthesizing the nat...Josh Chen2018-08-141-1/+1
* Commit before testing polymorphic equality eliminatorJosh Chen2018-08-121-0/+1
* Old application syntax incompatible with EisbachJosh Chen2018-08-071-4/+0
* Partway through changing function application syntax style.Josh Chen2018-08-061-9/+12
* Reorganize theoriesJosh Chen2018-08-041-35/+41
* Unit and Null types. Methods.Josh Chen2018-07-121-1/+2
* Universes implemented. Type rules modified accordingly. No more automatic der...Josh Chen2018-07-111-23/+12
* Alternative implementation of universes using meta-level numerals.Josh Chen2018-07-111-32/+43
* Pre-universe implementation commitJosh Chen2018-07-091-2/+23
* Library snapshot. Methods written, everything nicely organized.Josh Chen2018-07-071-1/+1
* Added attributes to type elimination rules, not sure if these will actually b...Josh Chen2018-07-061-3/+7
* Refactor HoTT_Methods.thy, proved more stuff with new methods.Josh Chen2018-07-031-1/+3
* Rewrote methods: wellformed now two lines, uses named theorems. New, more pow...Josh Chen2018-07-031-4/+5
* Library organization and formattingJosh Chen2018-06-271-1/+3
* Fixed wrong definition of snd_dep. Proved projection property of snd_dep. Add...Josh Chen2018-06-181-2/+1
* Removed all [simp] attributes, these will be added later when I set up the si...Josh Chen2018-06-181-1/+1
generated by cgit v1.2.3 (git 2.25.1) at 2024-11-19 14:03:43 +0000