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,
  ...
}

1 files changed, 1 insertions, 1 deletions

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 }}