aboutsummaryrefslogtreecommitdiff
Commit message (Expand)AuthorAgeFilesLines
* 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
* 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
| * | fix pathJosh Chen2020-07-171-2/+3
| * | testJosh Chen2020-07-173-8/+11
| * | check home varJosh Chen2020-07-171-1/+1
| * | change HOME env var, more testing...Josh Chen2020-07-171-1/+2
|/ /
* | more testJosh Chen2020-07-171-0/+1
* | more testingJosh Chen2020-07-173-14/+9
* | probe directoriesJosh Chen2020-07-161-1/+1
* | testJosh Chen2020-07-161-1/+2
* | try try againJosh Chen2020-07-163-7/+8
* | try againJosh Chen2020-07-161-6/+6
* | I think I figured out the problemJosh Chen2020-07-161-2/+1
generated by cgit v1.2.3 (git 2.25.1) at 2024-12-22 16:53:55 +0000