Skip to content

Commit fed7bf9

Browse files
committed
core: Sequential composition uses subgoals too
1 parent 9394d72 commit fed7bf9

File tree

1 file changed

+3
-2
lines changed

1 file changed

+3
-2
lines changed

prover/strategies/core.md

Lines changed: 3 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -63,10 +63,11 @@ cooled back into the sequence strategy.
6363

6464
```k
6565
syntax ResultStrategy ::= "#hole"
66-
rule <strategy> S1 . S2 => S1 ~> #hole . S2 ... </strategy>
66+
rule <strategy> S1 . S2 => S1 ~> #hole . S2 </strategy>
6767
requires notBool(isResultStrategy(S1))
6868
andBool notBool(isSequenceStrategy(S1))
69-
rule <strategy> S1:ResultStrategy ~> #hole . S2 => S1 . S2 ... </strategy>
69+
rule <claim> GOAL:Pattern </claim>
70+
<strategy> S1:ResultStrategy ~> #hole . S2 => subgoal(GOAL, S1 . S2) </strategy>
7071
```
7172

7273
The `noop` (no operation) strategy is the unit for sequential composition:

0 commit comments

Comments
 (0)