diff options
| author | Josh Chen | 2020-08-03 13:34:53 +0200 |
|---|---|---|
| committer | Josh Chen | 2020-08-03 13:34:53 +0200 |
| commit | 710f314a9ccb84cdd9df9bc8bf52482b8d1f5a56 (patch) | |
| tree | abbc3d847e17b9659b11eb8e4e2eda3430ba007a /spartan/core/context_tactical.ML | |
| parent | 70fd3f72ef8f9cc01a071250d94e8c25ecb04c1d (diff) | |
(FEAT) SIDE_CONDS tactical has additional argument specifying how many 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.
Diffstat (limited to '')
| -rw-r--r-- | spartan/core/context_tactical.ML | 4 |
1 files changed, 4 insertions, 0 deletions
diff --git a/spartan/core/context_tactical.ML b/spartan/core/context_tactical.ML index b5a6c00..0aa6f20 100644 --- a/spartan/core/context_tactical.ML +++ b/spartan/core/context_tactical.ML @@ -28,6 +28,7 @@ val CAPPEND': context_tactic' * context_tactic' -> context_tactic' val CTRY: context_tactic -> context_tactic val CREPEAT: context_tactic -> context_tactic val CREPEAT1: context_tactic -> context_tactic +val CREPEAT_N: int -> context_tactic -> context_tactic val CFILTER: (context_state -> bool) -> context_tactic -> context_tactic val CCHANGED: context_tactic -> context_tactic val CTHEN_ALL_NEW: context_tactic' * context_tactic' -> context_tactic' @@ -91,6 +92,9 @@ fun CREPEAT ctac = fun CREPEAT1 ctac = ctac CTHEN CREPEAT ctac +fun CREPEAT_N 0 _ = all_ctac + | CREPEAT_N n ctac = ctac CTHEN CREPEAT_N (n - 1) ctac + fun CFILTER pred ctac cst = ctac cst |> Seq.filter_results |