Commit message (Collapse) | Author | Age | Files | Lines | |
---|---|---|---|---|---|
* | renamings | Josh Chen | 2021-01-21 | 9 | -158/+154 |
| | |||||
* | Forgot to update ROOT | Josh Chen | 2021-01-19 | 1 | -1/+1 |
| | |||||
* | Bugfix: no longer repeatedly add duplicate rules to simpset | Josh Chen | 2021-01-19 | 1 | -1/+3 |
| | |||||
* | Swapped notation for metas (now ?) and holes (now {}), other notation and ↵ | Josh Chen | 2021-01-18 | 10 | -140/+143 |
| | | | | name changes. | ||||
* | Basic experiments adding reduction to the type checker | Josh Chen | 2020-09-23 | 6 | -118/+114 |
| | |||||
* | minor | Josh Chen | 2020-08-14 | 2 | -0/+8 |
| | |||||
* | reorganize | Josh Chen | 2020-08-14 | 4 | -64/+64 |
| | |||||
* | update license file list | Josh Chen | 2020-08-14 | 1 | -0/+4 |
| | |||||
* | (FEAT) Context data slots for known types and conditional type rules, as ↵ | Josh Chen | 2020-08-14 | 16 | -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 Chen | 2020-08-09 | 3 | -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 Chen | 2020-08-05 | 4 | -3/+63 |
| | | | | normalization in typechecking/elaboration. | ||||
* | (FEAT) SIDE_CONDS tactical has additional argument specifying how many ↵ | Josh Chen | 2020-08-03 | 7 | -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 theorems | Josh Chen | 2020-08-02 | 1 | -9/+9 |
| | |||||
* | (REF) Tweak attribute names in preparation for new logical introduction rule ↵ | Josh Chen | 2020-07-31 | 10 | -50/+52 |
| | | | | behavior | ||||
* | (FEAT) Term elaboration of assumption and goal statements. | Josh Chen | 2020-07-31 | 17 | -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 improvement | Josh Chen | 2020-07-28 | 1 | -2/+1 |
| | |||||
* | New `assuming` proof command for elaborated assumptions | Josh Chen | 2020-07-28 | 3 | -79/+118 |
| | |||||
* | Merge branch 'dev' | Josh Chen | 2020-07-27 | 9 | -146/+659 |
|\ | |||||
| * | Hook elaboration into assumptions mechanism | Josh Chen | 2020-07-27 | 8 | -79/+602 |
| | | |||||
| * | minor | Josh Chen | 2020-07-23 | 2 | -68/+57 |
| | | |||||
* | | update .gitignore | Josh Chen | 2020-07-27 | 1 | -1/+0 |
|/ | |||||
* | remove theory | Josh Chen | 2020-07-22 | 1 | -199/+0 |
| | |||||
* | begin work on pre-proof elaboration | Josh Chen | 2020-07-22 | 2 | -19/+218 |
| | |||||
* | minor | Josh Chen | 2020-07-21 | 1 | -1/+1 |
| | |||||
* | 1. Bugfix: implicits now properly name schematic variables. Fixes problems ↵ | Josh Chen | 2020-07-21 | 4 | -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/dev | Josh Chen | 2020-07-21 | 16 | -431/+603 |
|\ | | | | | Merge big diff on dev | ||||
| * | 1. Type-checking/inference now more principled, and the implementation is ↵ | Josh Chen | 2020-07-21 | 16 | -622/+394 |
| | | | | | | | | better. 2. Changed most tactics to context tactics. | ||||
| * | Checkpoint. THIS BUILD WILL FAIL | Josh Chen | 2020-07-16 | 6 | -51/+451 |
| | | |||||
* | | link | Josh Chen | 2020-07-17 | 1 | -1/+1 |
| | | |||||
* | | add build status | Josh Chen | 2020-07-17 | 1 | -1/+1 |
| | | |||||
* | | rename action | Josh Chen | 2020-07-17 | 1 | -1/+1 |
| | | |||||
* | | Merge pull request #7 from jaycech3n/ci-action | Josh Chen | 2020-07-17 | 3 | -8/+14 |
|\ \ | | | | | | | Ci action | ||||
| * | | looks like descriptions not allowed in workflow job yaml | Josh Chen | 2020-07-17 | 1 | -1/+0 |
| | | | |||||
| * | | final test push | Josh Chen | 2020-07-17 | 2 | -0/+2 |
| | | | |||||
| * | | fix path | Josh Chen | 2020-07-17 | 1 | -2/+3 |
| | | | |||||
| * | | test | Josh Chen | 2020-07-17 | 3 | -8/+11 |
| | | | |||||
| * | | check home var | Josh Chen | 2020-07-17 | 1 | -1/+1 |
| | | | |||||
| * | | change HOME env var, more testing... | Josh Chen | 2020-07-17 | 1 | -1/+2 |
|/ / | |||||
* | | more test | Josh Chen | 2020-07-17 | 1 | -0/+1 |
| | | |||||
* | | more testing | Josh Chen | 2020-07-17 | 3 | -14/+9 |
| | | |||||
* | | probe directories | Josh Chen | 2020-07-16 | 1 | -1/+1 |
| | | |||||
* | | test | Josh Chen | 2020-07-16 | 1 | -1/+2 |
| | | |||||
* | | try try again | Josh Chen | 2020-07-16 | 3 | -7/+8 |
| | | |||||
* | | try again | Josh Chen | 2020-07-16 | 1 | -6/+6 |
| | | |||||
* | | I think I figured out the problem | Josh Chen | 2020-07-16 | 1 | -2/+1 |
| | | |||||
* | | try ADD instead of RUN curl | Josh Chen | 2020-07-16 | 1 | -2/+1 |
| | | |||||
* | | will this parse now? | Josh Chen | 2020-07-16 | 1 | -1/+2 |
| | | |||||
* | | fix | Josh Chen | 2020-07-16 | 1 | -1/+1 |
| | | |||||
* | | download Isabelle from TUM archives | Josh Chen | 2020-07-16 | 1 | -2/+3 |
| | | |||||
* | | fix action path | Josh Chen | 2020-07-16 | 1 | -1/+1 |
| | |