From 710f314a9ccb84cdd9df9bc8bf52482b8d1f5a56 Mon Sep 17 00:00:00 2001
From: Josh Chen
Date: Mon, 3 Aug 2020 13:34:53 +0200
Subject: (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.
---
 spartan/core/context_tactical.ML | 4 ++++
 1 file changed, 4 insertions(+)

(limited to 'spartan/core/context_tactical.ML')

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
-- 
cgit v1.2.3