diff options
Diffstat (limited to 'spartan/core/context_tactical.ML')
| -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 |