aboutsummaryrefslogtreecommitdiff
Commit message (Collapse)AuthorAgeFilesLines
* HoTT_Test.thy should go in test/Josh Chen2018-08-181-1/+1
|
* Comments on subgoal test theoryJosh Chen2018-08-181-23/+29
|
* RenameJosh Chen2018-08-181-1/+2
|
* .gitignoreJosh Chen2018-08-181-0/+1
|
* Test theoriesJosh Chen2018-08-182-9/+64
|
* Misc formattingJosh Chen2018-08-183-3/+2
|
* Output formattingJosh Chen2018-08-181-1/+1
|
* Ignore more filesJosh Chen2018-08-181-0/+3
|
* Update licenseJosh Chen2018-08-181-1/+1
|
* Update test fileJosh Chen2018-08-181-113/+19
|
* Fixed mistake in Equal_elim and proof of rpathcomp_compJosh Chen2018-08-182-26/+26
|
* Update README.mdJosh Chen2018-08-171-9/+5
|
* Merge branch 'master' of github.com:jaycech3n/Isabelle-HoTTJosh Chen2018-08-171-2/+3
|\
| * Update README.mdJosh Chen2018-08-171-2/+3
| |
* | Fix silly mistakes in Coprod.thyJosh Chen2018-08-171-10/+10
| |
* | CleanupsJosh Chen2018-08-171-4/+4
|/
* Merge branch 'master' of github.com:jaycech3n/HoTTJosh Chen2018-08-171-0/+22
|\
| * Update README.mdJosh Chen2018-08-171-1/+6
| |
| * Add contactJosh Chen2018-08-171-1/+1
| |
| * Update README.mdJosh Chen2018-08-171-1/+1
| |
| * Update README.mdJosh Chen2018-08-171-1/+2
| |
| * Create README.mdJosh Chen2018-08-171-0/+16
| |
* | Properties of function compositionJosh Chen2018-08-171-24/+5
|/
* Remove test commit folderJosh Chen2018-08-171-1/+0
|
* Partway through updating proofs after the change of the function composition ↵Josh Chen2018-08-171-46/+11
| | | | definition
* Axiomatizations should be definitionsJosh Chen2018-08-171-4/+2
|
* Make function composition a definition instead of an axiomatization (should ↵Josh Chen2018-08-171-9/+1
| | | | not need to worry about preconditions)
* Change unnecessary axiomatization to a definitionJosh Chen2018-08-171-2/+2
|
* Testing with the new theoryJosh Chen2018-08-171-29/+25
|
* second testJosh Chen2018-08-161-0/+1
|
* test new machineJosh Chen2018-08-161-0/+2
|
* Some comments and reorganizationJosh Chen2018-08-162-24/+42
|
* Merge branch 'master' of github.com:jaycech3n/HoTTJosh Chen2018-08-160-0/+0
|\
| * Prod.thy now has the correct definitional equality structure rule. ↵Josh Chen2018-08-1613-59/+105
| | | | | | | | Definition of function composition and properties.
* | Prod.thy now has the correct definitional equality structure rule. ↵Josh Chen2018-08-1613-59/+105
|/ | | | Definition of function composition and properties.
* Rename to distinguish function and path composition; function composition ↵Josh Chen2018-08-155-101/+93
| | | | proofs, which have issues...
* Basic compute methodJosh Chen2018-08-155-12/+45
|
* Tweak proof methods, some type rules; add HoTT Book examplesJosh Chen2018-08-157-50/+87
|
* Function composition, rename path composition to differentiate the two.Josh Chen2018-08-152-20/+36
|
* Well-formation rules are back in the methods; new theory synthesizing the ↵Josh Chen2018-08-147-102/+174
| | | | natural number predecessor function.
* Equality inverse and composition done. Cleaned up methods and method example ↵Josh Chen2018-08-145-121/+215
| | | | theory.
* rcompose doneJosh Chen2018-08-137-78/+105
|
* Commit before testing polymorphic equality eliminatorJosh Chen2018-08-129-56/+108
|
* Rewriting projection functionsJosh Chen2018-08-082-211/+7
|
* TweaksJosh Chen2018-08-072-4/+9
|
* Old application syntax incompatible with EisbachJosh Chen2018-08-077-78/+74
|
* Experiment with polymorphic dependent eliminators, i.e. we leave type and ↵Josh Chen2018-08-072-14/+14
| | | | type family decorations implicit.
* Partway through changing function application syntax style.Josh Chen2018-08-067-138/+206
|
* CoproductJosh Chen2018-08-041-0/+61
|
* Reorganize theoriesJosh Chen2018-08-045-100/+130
|
generated by cgit v1.2.3 (git 2.25.1) at 2024-11-09 16:09:33 +0000