Skip to content

Commit

Permalink
docs(language): explanation for @Focus matching
Browse files Browse the repository at this point in the history
  • Loading branch information
kris7t committed Dec 12, 2024
1 parent 6222ddf commit 5a1fa86
Showing 1 changed file with 4 additions and 0 deletions.
Original file line number Diff line number Diff line change
Expand Up @@ -10,6 +10,10 @@ import builtin::annotations.
*
* If the parameter matches a single object, no new object will be created, but
* the postcondition of the decision rule will still be executed.
*
* Two `@focus` parameters can't match the same concrete object, i.e., they're
* always matched _monomorphically_. However, it's possible to match the same
* multi-object several times and split off several distinct objects from it.
*/
#pred focus().

Expand Down

0 comments on commit 5a1fa86

Please sign in to comment.