Skip to content

Commit 507cb90

Browse files
committed
core: cool sequences back in, so that subgoals are only generated for a single uncomposed strategy
1 parent 97dfb23 commit 507cb90

File tree

1 file changed

+2
-0
lines changed

1 file changed

+2
-0
lines changed

prover/strategies/core.md

Lines changed: 2 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -67,6 +67,8 @@ cooled back into the sequence strategy.
6767
<trace> _ => S1 </trace>
6868
requires notBool(isResultStrategy(S1))
6969
andBool notBool(isSequenceStrategy(S1))
70+
rule <claim> GOAL:Pattern </claim>
71+
<strategy> S1:SequenceStrategy ~> #hole . S2 => S1 . S2 </strategy>
7072
rule <claim> GOAL:Pattern </claim>
7173
<strategy> S1:ResultStrategy ~> #hole . S2 => subgoal(GOAL, S1 . S2) </strategy>
7274
```

0 commit comments

Comments
 (0)