aboutsummaryrefslogtreecommitdiff
path: root/spartan/core (unfollow)
Commit message (Collapse)AuthorFilesLines
2021-01-31rename things + some small changesJosh Chen17-3610/+0
2021-01-21renamingsJosh Chen3-37/+41
2021-01-19Bugfix: no longer repeatedly add duplicate rules to simpsetJosh Chen1-1/+3
2021-01-18Swapped notation for metas (now ?) and holes (now {}), other notation and ↵Josh Chen3-61/+57
name changes.
2020-09-23Basic experiments adding reduction to the type checkerJosh Chen3-45/+88
2020-08-14minorJosh Chen2-0/+8
2020-08-14reorganizeJosh Chen4-64/+64
2020-08-14(FEAT) Context data slots for known types and conditional type rules, as ↵Josh Chen10-125/+260
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.
2020-08-09(FEAT) Clean up typechecking/elaboration tactic: known_ctac should *solve* ↵Josh Chen2-11/+12
goals; resolving with conditional typing judgments (e.g. type family assumptions) is part of check_infer_step
2020-08-051. fix intros method. 2. Couple extra lemmas; good small test cases for ↵Josh Chen2-2/+3
normalization in typechecking/elaboration.
2020-08-03(FEAT) SIDE_CONDS tactical has additional argument specifying how many ↵Josh Chen5-23/+35
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.
2020-07-31(REF) Tweak attribute names in preparation for new logical introduction rule ↵Josh Chen4-19/+21
behavior
2020-07-31(FEAT) Term elaboration of assumption and goal statements.Josh Chen8-105/+250
. 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.
2020-07-28small improvementJosh Chen1-2/+1
2020-07-28New `assuming` proof command for elaborated assumptionsJosh Chen3-79/+118
2020-07-27Hook elaboration into assumptions mechanismJosh Chen6-29/+547
2020-07-23minorJosh Chen1-67/+56
2020-07-22remove theoryJosh Chen1-199/+0
2020-07-22begin work on pre-proof elaborationJosh Chen2-19/+218
2020-07-21minorJosh Chen1-1/+1
2020-07-211. Bugfix: implicits now properly name schematic variables. Fixes problems ↵Josh Chen2-16/+23
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.
2020-07-211. Type-checking/inference now more principled, and the implementation is ↵Josh Chen8-483/+257
better. 2. Changed most tactics to context tactics.
2020-07-16Checkpoint. THIS BUILD WILL FAILJosh Chen6-51/+451
2020-07-11Defined annotated terms to be used in future typechecking improvementsJosh Chen1-4/+7
2020-07-11rename fileJosh Chen1-2/+26
2020-07-09Non-annotated object lambdaJosh Chen1-20/+45
2020-07-081. Initial `Definition` keyword. 2. ifelse.Josh Chen2-13/+21
2020-06-19reorganizeJosh Chen26-1994/+50
2020-06-15rename foldersJosh Chen12-0/+1967
2020-06-031. Type information context dataJosh Chen2-2/+21
2. Small reformulations of rules 3. Bool
2020-05-30inhabitation coercion should be syntax, not logical constant!Josh Chen1-2/+2
2020-05-29fix Pi congruence ruleJosh Chen1-2/+2
2020-05-28notationJosh Chen1-0/+3
2020-05-28case distinctionJosh Chen3-1/+68
2020-05-28reorganize folder structureJosh Chen11-14/+14
2020-05-261. New congruence declarations for calculational reasoning. 2. Remove old ↵Josh Chen3-56/+87
elimination tactic.
2020-05-25fix implicits table merge mistakeJosh Chen1-1/+1
2020-05-25Lists + more reorganizingJosh Chen1-2/+7
2020-05-25Reorganize theory structure. In particular, the identity type moves out from ↵Josh Chen11-0/+2327
under Spartan to HoTT. Spartan now only has Pi and Sigma.
generated by cgit v1.2.3 (git 2.25.1) at 2024-07-09 12:57:00 +0000