aboutsummaryrefslogtreecommitdiff
path: root/HoTT_Base.thy (follow)
Commit message (Collapse)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
| | | | more proofs requiring the use of "U i: U (Suc i)", and shouldn't loop as much.
* tweak mixfix prioritiesJosh Chen2019-02-281-2/+2
|
* 1. Remove all type inference functionality (feature development moving to ↵Josh Chen2019-02-281-1/+10
| | | | | | another branch). 2. Eq.thy complete.
* Method "quantify" converts product inhabitation into Pure universal ↵Josh Chen2019-02-171-5/+8
| | | | statements. Also misc. cleanups.
* Put typing functionality into a .thy and clean up antiquotations, which ↵Josh Chen2019-02-111-47/+6
| | | | results in some reorganization of the theory import structure.
* restructure libraryJosh Chen2019-02-101-2/+2
|
* Explicit references in antiquotations in typing.ML. Move trace switch ↵Josh Chen2019-02-101-0/+3
| | | | definition to HoTT_Base.
* Type information storage functionality (assume_type, assume_types keywords) ↵Josh Chen2019-02-101-4/+34
| | | | done! Inference and pretty-printing for function composition done.
* 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
| | | | 2. Begin work on object-level type inference and input syntax help.
* 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 ↵Josh Chen2018-09-181-14/+15
| | | | handling universes. Commit for release 0.1.0!
* 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. ↵Josh Chen2018-08-161-1/+1
| | | | Definition of function composition and properties.
* Well-formation rules are back in the methods; new theory synthesizing the ↵Josh Chen2018-08-141-1/+1
| | | | natural number predecessor function.
* 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 ↵Josh Chen2018-07-111-23/+12
| | | | derivation of "A:U" from "a:A".
* 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 ↵Josh Chen2018-07-061-3/+7
| | | | be needed or useful later. Added [comp] attribute to be used by simplification met methods.
* 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 ↵Josh Chen2018-07-031-4/+5
| | | | powerful derive method. Used these to rewrite proofs.
* Library organization and formattingJosh Chen2018-06-271-1/+3
|
* Fixed wrong definition of snd_dep. Proved projection property of snd_dep. ↵Josh Chen2018-06-181-2/+1
| | | | Added type formation rules expressing necessity of the conditions.
* Removed all [simp] attributes, these will be added later when I set up the ↵Josh Chen2018-06-181-1/+1
| | | | simplifier. Proved simplification rule for dependent fst.
generated by cgit v1.2.3 (git 2.25.1) at 2024-07-03 17:49:44 +0000