diff --git a/prover/strategies/core.md b/prover/strategies/core.md index 4b330da04..77878fbb8 100644 --- a/prover/strategies/core.md +++ b/prover/strategies/core.md @@ -67,6 +67,8 @@ cooled back into the sequence strategy. _ => S1 requires notBool(isResultStrategy(S1)) andBool notBool(isSequenceStrategy(S1)) + rule GOAL:Pattern + S1:SequenceStrategy ~> #hole . S2 => S1 . S2 rule GOAL:Pattern S1:ResultStrategy ~> #hole . S2 => subgoal(GOAL, S1 . S2) ```