From 5a1fa86fb61134639f0661585dbebde788183090 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Krist=C3=B3f=20Marussy?= Date: Thu, 12 Dec 2024 17:34:57 +0100 Subject: [PATCH] docs(language): explanation for @focus matching --- .../tools/refinery/language/library/builtin/strategy.refinery | 4 ++++ 1 file changed, 4 insertions(+) diff --git a/subprojects/language/src/main/resources/tools/refinery/language/library/builtin/strategy.refinery b/subprojects/language/src/main/resources/tools/refinery/language/library/builtin/strategy.refinery index d2870e66..b3a32957 100644 --- a/subprojects/language/src/main/resources/tools/refinery/language/library/builtin/strategy.refinery +++ b/subprojects/language/src/main/resources/tools/refinery/language/library/builtin/strategy.refinery @@ -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().