aboutsummaryrefslogtreecommitdiff
Commit message (Expand)AuthorAgeFilesLines
* (broken) update hott for Isabelle 2021-1HEADmasterstuebinm2022-06-293-23/+24
* make mltt work with isabelle 2021-1stuebinm2022-06-295-12/+20
* 1. Thm/def statement display. 2. Syntax + computation proof.Josh Chen2021-06-283-8/+11
* begin refactoring EquivalenceJosh Chen2021-06-281-0/+458
* Bad practice huge commit:Josh Chen2021-06-2412-83/+164
* 1. Put universe level parameters first in automatic term definitions. 2. Add ...Josh Chen2021-06-234-10/+22
* update readmeJosh Chen2021-04-171-4/+3
* update CI to Isabelle 2021Josh Chen2021-04-171-2/+2
* Merge branch 'dev'Josh Chen2021-04-174-2/+29
|\
| * Patch proof. Now works on Isabelle2021.Josh Chen2021-04-171-1/+1
| * Small fix: extraneous variableJosh Chen2021-04-171-1/+1
| * start hprop stuffJosh Chen2021-04-102-0/+27
* | small renameJosh Chen2021-04-101-3/+3
* | update Isabelle2020 URL in DockerfileJosh Chen2021-04-101-1/+1
|/
* update readmeJosh Chen2021-02-011-11/+8
* rename things + some small changesJosh Chen2021-01-3125-163/+66
* renamingsJosh Chen2021-01-219-158/+154
* Forgot to update ROOTJosh Chen2021-01-191-1/+1
* Bugfix: no longer repeatedly add duplicate rules to simpsetJosh Chen2021-01-191-1/+3
* Swapped notation for metas (now ?) and holes (now {}), other notation and nam...Josh Chen2021-01-1810-140/+143
* Basic experiments adding reduction to the type checkerJosh Chen2020-09-236-118/+114
* minorJosh Chen2020-08-142-0/+8
* reorganizeJosh Chen2020-08-144-64/+64
* update license file listJosh Chen2020-08-141-0/+4
* (FEAT) Context data slots for known types and conditional type rules, as well...Josh Chen2020-08-1416-178/+313
* (FEAT) Clean up typechecking/elaboration tactic: known_ctac should *solve* go...Josh Chen2020-08-093-18/+18
* 1. fix intros method. 2. Couple extra lemmas; good small test cases for norma...Josh Chen2020-08-054-3/+63
* (FEAT) SIDE_CONDS tactical has additional argument specifying how many initia...Josh Chen2020-08-037-38/+42
* rename some theoremsJosh Chen2020-08-021-9/+9
* (REF) Tweak attribute names in preparation for new logical introduction rule ...Josh Chen2020-07-3110-50/+52
* (FEAT) Term elaboration of assumption and goal statements.Josh Chen2020-07-3117-528/+670
* small improvementJosh Chen2020-07-281-2/+1
* New `assuming` proof command for elaborated assumptionsJosh Chen2020-07-283-79/+118
* Merge branch 'dev'Josh Chen2020-07-279-146/+659
|\
| * Hook elaboration into assumptions mechanismJosh Chen2020-07-278-79/+602
| * minorJosh Chen2020-07-232-68/+57
* | update .gitignoreJosh Chen2020-07-271-1/+0
|/
* remove theoryJosh Chen2020-07-221-199/+0
* begin work on pre-proof elaborationJosh Chen2020-07-222-19/+218
* minorJosh Chen2020-07-211-1/+1
* 1. Bugfix: implicits now properly name schematic variables. Fixes problems ca...Josh Chen2020-07-214-35/+45
* Merge pull request #8 from jaycech3n/devJosh Chen2020-07-2116-431/+603
|\
| * 1. Type-checking/inference now more principled, and the implementation is bet...Josh Chen2020-07-2116-622/+394
| * Checkpoint. THIS BUILD WILL FAILJosh Chen2020-07-166-51/+451
* | linkJosh Chen2020-07-171-1/+1
* | add build statusJosh Chen2020-07-171-1/+1
* | rename actionJosh Chen2020-07-171-1/+1
* | Merge pull request #7 from jaycech3n/ci-actionJosh Chen2020-07-173-8/+14
|\ \
| * | looks like descriptions not allowed in workflow job yamlJosh Chen2020-07-171-1/+0
| * | final test pushJosh Chen2020-07-172-0/+2
generated by cgit v1.2.3 (git 2.25.1) at 2024-04-19 10:17:15 +0000