From a7563156f1ea9ca71c2d4cd0de4bad67f0f99b30 Mon Sep 17 00:00:00 2001
From: Jon French
Date: Wed, 16 May 2018 15:44:19 +0100
Subject: Add support for inline val-spec declaration for mappings

This means that a mapping which formerly had to be pre-declared like

val name : a <-> b
...
mapping name {
  x <-> y,
  ...
}

can now be shortened to

mapping name : a <-> b {
  x <-> y,
  ...
}
---
 language/sail.ott | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'language')

diff --git a/language/sail.ott b/language/sail.ott
index 83d80be8..1b1e4d48 100644
--- a/language/sail.ott
+++ b/language/sail.ott
@@ -1017,7 +1017,7 @@ mapcl :: 'MCL_' ::=
 mapdef :: 'MD_' ::=
   {{ com mapping definition (bidirectional pattern-match function) }}
   {{ aux _ annot }} {{ auxparam 'a }}
-  | mapping id = { mapcl1 , ... , mapcln } :: :: mapping {{ texlong }}
+  | mapping id tannot_opt = { mapcl1 , ... , mapcln } :: :: mapping {{ texlong }}
 
 letbind :: 'LB_' ::=
   {{ com let binding }}
-- 
cgit v1.2.3