core: cool sequences back in, so that subgoals are only generated for…

… a single uncomposed strategy
kframework · Apr 22, 2020 · 2491890 · 2491890
1 parent 0b8678e
commit 2491890
Showing 1 changed file with 2 additions and 0 deletions.
diff --git a/prover/strategies/core.md b/prover/strategies/core.md
@@ -67,6 +67,8 @@ cooled back into the sequence strategy.
        <trace> _ => S1 </trace>
     requires notBool(isResultStrategy(S1))
      andBool notBool(isSequenceStrategy(S1))
+  rule <claim> GOAL:Pattern </claim>
+       <strategy> S1:SequenceStrategy ~> #hole . S2 => S1 . S2 </strategy>
   rule <claim> GOAL:Pattern </claim>
        <strategy> S1:ResultStrategy ~> #hole . S2 => subgoal(GOAL, S1 . S2) </strategy>
 ```