aboutsummaryrefslogtreecommitdiff
Commit message (Collapse)AuthorAgeFilesLines
* (broken) update hott for Isabelle 2021-1HEADmasterstuebinm2022-06-293-23/+24
| | | | | | | | | this just replaces all instance of `this` with instances of `infer`. Unfortunately, it looks likes something else also broke, and I have no idea what it is (but the proof for equiv_if_equal fails). Sadly this means we can't get to univalence for now … (but rn I'm too tired to try anything else with it)
* make mltt work with isabelle 2021-1stuebinm2022-06-295-12/+20
| | | | | | | | | | notably, this modifies the proof method `this`: the previous version of it no longer works with cconv.ML (borrowed from HOL), so now it's just a call to the simplifier, which does work. Unfortunately the new `this` can otherwise do less than the old one (it does not instantiate schematic variables), so the old one is now available as `infer` instead.
* 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. Rudimentary prototype definitional package 2. Started univalence 3. Various compatibility fixes and new theory stubs 4. Updated ROOT file
* 1. Put universe level parameters first in automatic term definitions. 2. Add ↵Josh Chen2021-06-234-10/+22
| | | | debugging to typechecker
* 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 ↵Josh Chen2021-01-1810-140/+143
| | | | name changes.
* 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 ↵Josh Chen2020-08-1416-178/+313
| | | | | | | | | | | | | well as a separate one for judgmental equality rules. (REF) Goal statement assumptions are now put into the new context data slots. (FEAT) `assuming` Isar keyword—like `assume` but puts assumptions into context data. (REF) Typechecking and all other tactics refactored to use type information from the context data, as opposed to looking at all facts visible in context. MINOR INCOMPATIBILITY: facts that were implicitly used in proofs now have to be annotated with [type] to make them visible throughout the context, else explicitly passed to methods via `using`, or declared with `assuming`. (REF) Fixed incompatibilities in theories.
* (FEAT) Clean up typechecking/elaboration tactic: known_ctac should *solve* ↵Josh Chen2020-08-093-18/+18
| | | | goals; resolving with conditional typing judgments (e.g. type family assumptions) is part of check_infer_step
* 1. fix intros method. 2. Couple extra lemmas; good small test cases for ↵Josh Chen2020-08-054-3/+63
| | | | normalization in typechecking/elaboration.
* (FEAT) SIDE_CONDS tactical has additional argument specifying how many ↵Josh Chen2020-08-037-38/+42
| | | | | | | | initial subgoals to skip applying the side condition solver to. (FEAT) `intro`, `intros` methods for "logical introduction rules" (as opposed to typechecking `intr` attribute), only works on conclusions with rigid type. (FEAT) CREPEAT_N bounded repetition tactical, used in `intros n` method.
* 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
| | | | behavior
* (FEAT) Term elaboration of assumption and goal statements.Josh Chen2020-07-3117-528/+670
| | | | | | | | | | | | | | | | | | | | . spartan/core/goals.ML . spartan/core/elaboration.ML . spartan/core/elaborated_statement.ML (FEAT) More context tacticals and search tacticals. . spartan/core/context_tactical.ML (FEAT) Improved subgoal focus. Moves fully elaborated assumptions into the context (MINOR INCOMPATIBILITY). . spartan/core/focus.ML (FIX) Normalize facts in order to be able to resolve properly. . spartan/core/typechecking.ML (MAIN) New definitions. (MAIN) Renamed theories and theorems. (MAIN) Refactor theories to fit new features.
* 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 ↵Josh Chen2020-07-214-35/+45
| | | | caused by variable name clashes. 2. reduce method now more principled: restricts to repeating on first subgoal. 3. An example declarative proof in Equivalence.thy.
* Merge pull request #8 from jaycech3n/devJosh Chen2020-07-2116-431/+603
|\ | | | | Merge big diff on dev
| * 1. Type-checking/inference now more principled, and the implementation is ↵Josh Chen2020-07-2116-622/+394
| | | | | | | | better. 2. Changed most tactics to context tactics.
| * 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
|\ \ | | | | | | Ci action
| * | 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-05-02 00:51:18 +0000