aboutsummaryrefslogtreecommitdiff
path: root/spartan (unfollow)
Commit message (Collapse)AuthorFilesLines
2021-01-31rename things + some small changesJosh Chen20-4027/+0
2021-01-21renamingsJosh Chen6-45/+49
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 Chen6-71/+67
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 Chen13-130/+266
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 Chen7-29/+31
behavior
2020-07-31(FEAT) Term elaboration of assumption and goal statements.Josh Chen11-122/+268
. 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 Chen11-505/+285
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 Chen4-40/+62
2020-07-081. Initial `Definition` keyword. 2. ifelse.Josh Chen5-28/+76
2020-06-19reorganizeJosh Chen26-1994/+50
2020-06-15remove old folderJosh Chen3-372/+0
2020-06-15rename foldersJosh Chen15-0/+2339
2020-06-031. Type information context dataJosh Chen4-5/+32
2. Small reformulations of rules 3. Bool
2020-06-01reorganize and add some materialJosh Chen1-41/+59
2020-05-31more listJosh Chen1-8/+28
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-28bit more materialJosh Chen1-10/+14
2020-05-28notationJosh Chen1-0/+3
2020-05-28more List and MaybeJosh Chen3-7/+22
2020-05-28case distinctionJosh Chen3-1/+68
2020-05-28reorganize folder structureJosh Chen11-14/+14
2020-05-27change variable name in elim rules and fix small mistakeJosh Chen3-23/+19
2020-05-271. Define Maybe in terms of other types. 2. Move More_Types to SpartanJosh Chen2-28/+134
2020-05-261. New congruence declarations for calculational reasoning. 2. Remove old ↵Josh Chen3-56/+87
elimination tactic.
2020-05-26Maybe and more ListJosh Chen2-7/+123
2020-05-25notationJosh Chen1-0/+4
2020-05-25fix implicits table merge mistakeJosh Chen1-1/+1
2020-05-25Lists + more reorganizingJosh Chen2-2/+86
2020-05-25Reorganize theory structure. In particular, the identity type moves out from ↵Josh Chen14-889/+15
under Spartan to HoTT. Spartan now only has Pi and Sigma.
2020-05-25slightly nicer homotopy proofs with calculationsJosh Chen2-30/+16
2020-05-25`refl` and `this` methodsJosh Chen1-8/+20
generated by cgit v1.2.3 (git 2.25.1) at 2024-07-01 14:58:13 +0000