From 4f20163965e7c336f28740628fa9d64528006861 Mon Sep 17 00:00:00 2001
From: Brian Campbell
Date: Tue, 11 Dec 2018 11:54:36 +0000
Subject: Initial attempt at using termination measures in Coq This only
 applies to recursive functions and uses the termination measure merely as a
 limit to the recursive call depth, rather than proving the measure correct.

---
 language/sail.ott | 4 +++-
 1 file changed, 3 insertions(+), 1 deletion(-)

(limited to 'language')

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 }}
-- 
cgit v1.2.3