summaryrefslogtreecommitdiff
path: root/language/l2.ott
diff options
context:
space:
mode:
Diffstat (limited to 'language/l2.ott')
-rw-r--r--language/l2.ott2
1 files changed, 1 insertions, 1 deletions
diff --git a/language/l2.ott b/language/l2.ott
index 96a30265..96483b90 100644
--- a/language/l2.ott
+++ b/language/l2.ott
@@ -197,7 +197,7 @@ base_effect :: 'BE_' ::=
| nondet :: :: nondet {{ com nondeterminism from intra-instruction parallelism }}
| escape :: :: escape {{ com Tracking of expressions and functions that might call exit }}
| lset :: :: lset {{ com Local mutation happend; not user-writable }}
-
+ | lret :: :: lret {{ com Local return happened; not user-writable }}
effect :: 'Effect_' ::=
{{ com effect set, of kind Effects }}