aboutsummaryrefslogtreecommitdiff
Commit message (Expand)AuthorAgeFilesLines
...
* | Should write the correct rule for Ord_leq_min. Another exercise.Josh Chen2018-08-302-2/+18
* | Add leq relation to meta-ordinals, it helps with proofsJosh Chen2018-08-302-7/+12
* | Rename LICENSE.md to LICENSEJosh Chen2018-08-211-0/+0
* | Create LICENSE.mdJosh Chen2018-08-211-0/+165
|/
* Forgot to add the theories for Empty and UnitJosh Chen2018-08-182-0/+63
* Distinguish the typing judgmentJosh Chen2018-08-181-2/+1
* Move Empty and Unit types to their own theoriesJosh Chen2018-08-183-32/+2
* .gitignoreJosh Chen2018-08-181-0/+7
* Update Test.thyJosh Chen2018-08-181-12/+12
* Reorganize methodsJosh Chen2018-08-1813-94/+98
* Regrouping type rulesJosh Chen2018-08-1816-108/+102
* 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
* Axiomatizations should be definitionsJosh Chen2018-08-171-4/+2
* Make function composition a definition instead of an axiomatization (should n...Josh Chen2018-08-171-9/+1
* 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. Definition...Josh Chen2018-08-1613-59/+105
* | Prod.thy now has the correct definitional equality structure rule. Definition...Josh Chen2018-08-1613-59/+105
|/
* Rename to distinguish function and path composition; function composition pro...Josh Chen2018-08-155-101/+93
* 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
generated by cgit v1.2.3 (git 2.25.1) at 2024-12-24 03:36:08 +0000