| Commit message (Collapse) | Author | Age | Files | Lines |
|---|
| |
|
|
|
|
|
|
|
| |
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)
|
| |
|
|
|
|
|
| |
1. Rudimentary prototype definitional package
2. Started univalence
3. Various compatibility fixes and new theory stubs
4. Updated ROOT file
|
| | |
|
| | |
|
| | |
|
| |
|
|
| |
name changes.
|
| | |
|
| |
|
|
|
|
|
|
|
|
|
|
|
| |
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.
|
| |
|
|
| |
normalization in typechecking/elaboration.
|
| |
|
|
|
|
|
|
| |
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.
|
| |
|
|
| |
behavior
|
| |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
. 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.
|
| | |
|
| |
|
|
| |
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.
|
| |
|
|
| |
better. 2. Changed most tactics to context tactics.
|
| | |
|
| | |
|
| | |
|
| | |
|
| | |
|
| | |
|
| | |
|
| | |
|
| | |
|
|
|
under Spartan to HoTT. Spartan now only has Pi and Sigma.
|
