summaryrefslogtreecommitdiff
path: root/language
diff options
context:
space:
mode:
Diffstat (limited to 'language')
-rw-r--r--language/sail.ott4
1 files changed, 3 insertions, 1 deletions
diff --git a/language/sail.ott b/language/sail.ott
index a0b02a1c..04207658 100644
--- a/language/sail.ott
+++ b/language/sail.ott
@@ -847,9 +847,11 @@ tannot_opt :: 'Typ_annot_opt_' ::=
rec_opt :: 'Rec_' ::=
{{ com optional recursive annotation for functions }}
+ {{ auxparam 'a }}
{{ aux _ l }}
| :: :: nonrec {{ com non-recursive }}
- | rec :: :: rec {{ com recursive }}
+ | rec :: :: rec {{ com recursive without termination measure }}
+ | { pat -> exp } :: :: measure {{ com recursive with termination measure }}
effect_opt :: 'Effect_opt_' ::=
{{ com optional effect annotation for functions }}