Changed syntax of derived types to "newtype"

Added parsing of constraints (beyond parsing is yet to come)

11 files changed, 799 insertions, 720 deletions

diff --git a/Source/Dafny/Dafny.atg b/Source/Dafny/Dafny.atg
index d3fad9e6..3811cbbf 100644
--- a/Source/Dafny/Dafny.atg
+++ b/Source/Dafny/Dafny.atg
@@ -143,6 +143,11 @@ bool IsIdentParen() {
   return la.kind == _ident && x.kind == _openparen;

 }

 

+bool IsIdentColon() {

+  Token x = scanner.Peek();

+  return la.kind == _ident && x.kind == _colon;

+}

+

 bool SemiFollowsCall(bool allowSemi, Expression e) {

   return allowSemi && la.kind == _semi &&

     (e is FunctionCallExpr || e is ApplyExpr ||

@@ -237,6 +242,7 @@ Dafny
   { SubModuleDecl<defaultModule, out submodule> (. defaultModule.TopLevelDecls.Add(submodule); .)

   | ClassDecl<defaultModule, out c>             (. defaultModule.TopLevelDecls.Add(c); .)

   | DatatypeDecl<defaultModule, out dt>         (. defaultModule.TopLevelDecls.Add(dt); .)

+  | NewtypeDecl<defaultModule, out td>          (. defaultModule.TopLevelDecls.Add(td); .)

   | OtherTypeDecl<defaultModule, out td>        (. defaultModule.TopLevelDecls.Add(td); .)

   | IteratorDecl<defaultModule, out iter>       (. defaultModule.TopLevelDecls.Add(iter); .)

   | TraitDecl<defaultModule, out trait>    (. defaultModule.TopLevelDecls.Add(trait); .)

@@ -278,8 +284,9 @@ SubModuleDecl<ModuleDefinition parent, out ModuleDecl submodule>
        "{"                                       (. module.BodyStartTok = t; .)

         { SubModuleDecl<module, out sm>                (. module.TopLevelDecls.Add(sm); .)

         | ClassDecl<module, out c>                     (. module.TopLevelDecls.Add(c); .)

-        | TraitDecl<module, out trait>            (. module.TopLevelDecls.Add(trait); .)

+        | TraitDecl<module, out trait>                 (. module.TopLevelDecls.Add(trait); .)

 		| DatatypeDecl<module, out dt>                 (. module.TopLevelDecls.Add(dt); .)

+        | NewtypeDecl<module, out td>                  (. module.TopLevelDecls.Add(td); .)

         | OtherTypeDecl<module, out td>                (. module.TopLevelDecls.Add(td); .)

         | IteratorDecl<module, out iter>               (. module.TopLevelDecls.Add(iter); .)

         | ClassMemberDecl<namedModuleDefaultClassMembers, false>

@@ -446,8 +453,33 @@ FieldDecl<.MemberModifiers mmod, List<MemberDecl/*!*/>/*!*/ mm.>
   }

   SYNC ";"

   .

-OtherTypeDecl<ModuleDefinition/*!*/ module, out TopLevelDecl td>

-= (. IToken/*!*/ id;

+NewtypeDecl<ModuleDefinition module, out TopLevelDecl td>

+= (. IToken id, bvId;

+     Attributes attrs = null;

+     td = null;

+     Type baseType;

+     Expression wh;

+  .)

+  "newtype"

+  { Attribute<ref attrs> }

+  NoUSIdent<out id>

+  "="

+  ( IF(IsIdentColon())

+    NoUSIdent<out bvId>

+    ":"

+    Type<out baseType>

+    "where"

+    Expression<out wh, false, true>  (. td = new DerivedTypeDecl(id, id.val, module, new BoundVar(bvId, bvId.val, baseType), wh, attrs); .)

+  | Type<out baseType>               (. td = new DerivedTypeDecl(id, id.val, module, baseType, attrs); .)

+  )

+  [ SYNC ";"

+      // In a future version of Dafny, including the following warning message:

+      //     (. errors.Warning(t, "the semi-colon that used to terminate an opaque-type declaration has been deprecated; in the new syntax, just leave off the semi-colon"); .)

+      // And in a version after that, don't allow the semi-colon at all.

+  ]

+  .

+OtherTypeDecl<ModuleDefinition module, out TopLevelDecl td>

+= (. IToken id;

      Attributes attrs = null;

      var eqSupport = TypeParameter.EqualitySupportValue.Unspecified;

      var typeArgs = new List<TypeParameter>();

@@ -462,13 +494,7 @@ OtherTypeDecl<ModuleDefinition/*!*/ module, out TopLevelDecl td>
   |

     [ GenericParameters<typeArgs> ]

     [ "="

-      ( "new"

-        Type<out ty>             (. if (typeArgs.Count != 0) {

-                                      SemErr(typeArgs[0].tok, "a derived type is not allowed type arguments");

-                                    }

-                                    td = new DerivedTypeDecl(id, id.val, module, ty, attrs); .)

-      | Type<out ty>             (. td = new TypeSynonymDecl(id, id.val, typeArgs, module, ty, attrs); .)

-      )

+      Type<out ty>             (. td = new TypeSynonymDecl(id, id.val, typeArgs, module, ty, attrs); .)

     ]

   )                            (. if (td == null) {

                                     td = new OpaqueTypeDecl(id, id.val, module, eqSupport, typeArgs, attrs);

diff --git a/Source/Dafny/DafnyAst.cs b/Source/Dafny/DafnyAst.cs
index 6fec41e4..7fa9dfb4 100644
--- a/Source/Dafny/DafnyAst.cs
+++ b/Source/Dafny/DafnyAst.cs
@@ -2201,6 +2201,8 @@ namespace Microsoft.Dafny {
   public class DerivedTypeDecl : TopLevelDecl, RedirectingTypeDecl

   {

     public readonly Type BaseType;

+    public readonly BoundVar Var;  // can be null (if non-null, Var.Type == BaseType)

+    public readonly Expression Constraint;  // is null iff Var is

     public DerivedTypeDecl(IToken tok, string name, ModuleDefinition module, Type baseType, Attributes attributes)

       : base(tok, name, module, new List<TypeParameter>(), attributes) {

       Contract.Requires(tok != null);

@@ -2209,6 +2211,16 @@ namespace Microsoft.Dafny {
       Contract.Requires(baseType != null);

       BaseType = baseType;

     }

+    public DerivedTypeDecl(IToken tok, string name, ModuleDefinition module, BoundVar bv, Expression constraint, Attributes attributes)

+      : base(tok, name, module, new List<TypeParameter>(), attributes) {

+      Contract.Requires(tok != null);

+      Contract.Requires(name != null);

+      Contract.Requires(module != null);

+      Contract.Requires(bv != null && bv.Type != null);

+      BaseType = bv.Type;

+      Var = bv;

+      Constraint = constraint;

+    }

     IToken RedirectingTypeDecl.Tok { get { return tok; } }

     string RedirectingTypeDecl.Name { get { return Name; } }

   }

diff --git a/Source/Dafny/Parser.cs b/Source/Dafny/Parser.cs
index cfa18e56..b537752a 100644
--- a/Source/Dafny/Parser.cs
+++ b/Source/Dafny/Parser.cs
@@ -32,7 +32,7 @@ public class Parser {
 	public const int _closeparen = 16;

 	public const int _star = 17;

 	public const int _notIn = 18;

-	public const int maxT = 129;

+	public const int maxT = 130;

 

 	const bool T = true;

 	const bool x = false;

@@ -174,6 +174,11 @@ bool IsIdentParen() {
   return la.kind == _ident && x.kind == _openparen;

 }

 

+bool IsIdentColon() {

+  Token x = scanner.Peek();

+  return la.kind == _ident && x.kind == _colon;

+}

+

 bool SemiFollowsCall(bool allowSemi, Expression e) {

   return allowSemi && la.kind == _semi &&

     (e is FunctionCallExpr || e is ApplyExpr ||

@@ -303,11 +308,16 @@ bool CloseOptionalBrace(bool usesOptionalBrace) {
 				break;

 			}

 			case 38: {

+				NewtypeDecl(defaultModule, out td);

+				defaultModule.TopLevelDecls.Add(td); 

+				break;

+			}

+			case 40: {

 				OtherTypeDecl(defaultModule, out td);

 				defaultModule.TopLevelDecls.Add(td); 

 				break;

 			}

-			case 41: {

+			case 42: {

 				IteratorDecl(defaultModule, out iter);

 				defaultModule.TopLevelDecls.Add(iter); 

 				break;

@@ -317,7 +327,7 @@ bool CloseOptionalBrace(bool usesOptionalBrace) {
 				defaultModule.TopLevelDecls.Add(trait); 

 				break;

 			}

-			case 31: case 32: case 36: case 47: case 48: case 49: case 50: case 51: case 67: case 68: case 69: {

+			case 31: case 32: case 36: case 48: case 49: case 50: case 51: case 52: case 68: case 69: case 70: {

 				ClassMemberDecl(membersDefaultClass, false);

 				break;

 			}

@@ -390,16 +400,21 @@ bool CloseOptionalBrace(bool usesOptionalBrace) {
 					break;

 				}

 				case 38: {

+					NewtypeDecl(module, out td);

+					module.TopLevelDecls.Add(td); 

+					break;

+				}

+				case 40: {

 					OtherTypeDecl(module, out td);

 					module.TopLevelDecls.Add(td); 

 					break;

 				}

-				case 41: {

+				case 42: {

 					IteratorDecl(module, out iter);

 					module.TopLevelDecls.Add(iter); 

 					break;

 				}

-				case 31: case 32: case 36: case 47: case 48: case 49: case 50: case 51: case 67: case 68: case 69: {

+				case 31: case 32: case 36: case 48: case 49: case 50: case 51: case 52: case 68: case 69: case 70: {

 					ClassMemberDecl(namedModuleDefaultClassMembers, false);

 					break;

 				}

@@ -432,7 +447,7 @@ bool CloseOptionalBrace(bool usesOptionalBrace) {
 				}

 			}

 			if (la.kind == 8) {

-				while (!(la.kind == 0 || la.kind == 8)) {SynErr(130); Get();}

+				while (!(la.kind == 0 || la.kind == 8)) {SynErr(131); Get();}

 				Get();

 			}

 			if (submodule == null) {

@@ -441,7 +456,7 @@ bool CloseOptionalBrace(bool usesOptionalBrace) {
 			 submodule = new AliasModuleDecl(idPath, id, parent, opened);

 			}

 			

-		} else SynErr(131);

+		} else SynErr(132);

 	}

 

 	void ClassDecl(ModuleDefinition/*!*/ module, out ClassDecl/*!*/ c) {

@@ -454,13 +469,13 @@ bool CloseOptionalBrace(bool usesOptionalBrace) {
 		List<MemberDecl/*!*/> members = new List<MemberDecl/*!*/>();

 		IToken bodyStart;

 		

-		while (!(la.kind == 0 || la.kind == 28)) {SynErr(132); Get();}

+		while (!(la.kind == 0 || la.kind == 28)) {SynErr(133); Get();}

 		Expect(28);

 		while (la.kind == 13) {

 			Attribute(ref attrs);

 		}

 		NoUSIdent(out id);

-		if (la.kind == 45) {

+		if (la.kind == 46) {

 			GenericParameters(typeArgs);

 		}

 		if (la.kind == 29) {

@@ -489,18 +504,18 @@ bool CloseOptionalBrace(bool usesOptionalBrace) {
 		IToken bodyStart = Token.NoToken;  // dummy assignment

 		bool co = false;

 		

-		while (!(la.kind == 0 || la.kind == 33 || la.kind == 34)) {SynErr(133); Get();}

+		while (!(la.kind == 0 || la.kind == 33 || la.kind == 34)) {SynErr(134); Get();}

 		if (la.kind == 33) {

 			Get();

 		} else if (la.kind == 34) {

 			Get();

 			co = true; 

-		} else SynErr(134);

+		} else SynErr(135);

 		while (la.kind == 13) {

 			Attribute(ref attrs);

 		}

 		NoUSIdent(out id);

-		if (la.kind == 45) {

+		if (la.kind == 46) {

 			GenericParameters(typeArgs);

 		}

 		Expect(25);

@@ -511,7 +526,7 @@ bool CloseOptionalBrace(bool usesOptionalBrace) {
 			DatatypeMemberDecl(ctors);

 		}

 		if (la.kind == 8) {

-			while (!(la.kind == 0 || la.kind == 8)) {SynErr(135); Get();}

+			while (!(la.kind == 0 || la.kind == 8)) {SynErr(136); Get();}

 			Get();

 		}

 		if (co) {

@@ -524,52 +539,73 @@ bool CloseOptionalBrace(bool usesOptionalBrace) {
 		

 	}

 

-	void OtherTypeDecl(ModuleDefinition/*!*/ module, out TopLevelDecl td) {

-		IToken/*!*/ id;

+	void NewtypeDecl(ModuleDefinition module, out TopLevelDecl td) {

+		IToken id, bvId;

+		Attributes attrs = null;

+		td = null;

+		Type baseType;

+		Expression wh;

+		

+		Expect(38);

+		while (la.kind == 13) {

+			Attribute(ref attrs);

+		}

+		NoUSIdent(out id);

+		Expect(25);

+		if (IsIdentColon()) {

+			NoUSIdent(out bvId);

+			Expect(7);

+			Type(out baseType);

+			Expect(39);

+			Expression(out wh, false, true);

+			td = new DerivedTypeDecl(id, id.val, module, new BoundVar(bvId, bvId.val, baseType), wh, attrs); 

+		} else if (StartOf(3)) {

+			Type(out baseType);

+			td = new DerivedTypeDecl(id, id.val, module, baseType, attrs); 

+		} else SynErr(137);

+		if (la.kind == 8) {

+			while (!(la.kind == 0 || la.kind == 8)) {SynErr(138); Get();}

+			Get();

+		}

+	}

+

+	void OtherTypeDecl(ModuleDefinition module, out TopLevelDecl td) {

+		IToken id;

 		Attributes attrs = null;

 		var eqSupport = TypeParameter.EqualitySupportValue.Unspecified;

 		var typeArgs = new List<TypeParameter>();

 		td = null;

 		Type ty;

 		

-		Expect(38);

+		Expect(40);

 		while (la.kind == 13) {

 			Attribute(ref attrs);

 		}

 		NoUSIdent(out id);

 		if (la.kind == 15) {

 			Get();

-			Expect(39);

+			Expect(41);

 			Expect(16);

 			eqSupport = TypeParameter.EqualitySupportValue.Required; 

-			if (la.kind == 45) {

+			if (la.kind == 46) {

 				GenericParameters(typeArgs);

 			}

-		} else if (StartOf(3)) {

-			if (la.kind == 45) {

+		} else if (StartOf(4)) {

+			if (la.kind == 46) {

 				GenericParameters(typeArgs);

 			}

 			if (la.kind == 25) {

 				Get();

-				if (la.kind == 40) {

-					Get();

-					Type(out ty);

-					if (typeArgs.Count != 0) {

-					 SemErr(typeArgs[0].tok, "a derived type is not allowed type arguments");

-					}

-					td = new DerivedTypeDecl(id, id.val, module, ty, attrs); 

-				} else if (StartOf(4)) {

-					Type(out ty);

-					td = new TypeSynonymDecl(id, id.val, typeArgs, module, ty, attrs); 

-				} else SynErr(136);

+				Type(out ty);

+				td = new TypeSynonymDecl(id, id.val, typeArgs, module, ty, attrs); 

 			}

-		} else SynErr(137);

+		} else SynErr(139);

 		if (td == null) {

 		 td = new OpaqueTypeDecl(id, id.val, module, eqSupport, typeArgs, attrs);

 		}

 		

 		if (la.kind == 8) {

-			while (!(la.kind == 0 || la.kind == 8)) {SynErr(138); Get();}

+			while (!(la.kind == 0 || la.kind == 8)) {SynErr(140); Get();}

 			Get();

 		}

 	}

@@ -598,19 +634,19 @@ bool CloseOptionalBrace(bool usesOptionalBrace) {
 		IToken bodyStart = Token.NoToken;

 		IToken bodyEnd = Token.NoToken;

 		

-		while (!(la.kind == 0 || la.kind == 41)) {SynErr(139); Get();}

-		Expect(41);

+		while (!(la.kind == 0 || la.kind == 42)) {SynErr(141); Get();}

+		Expect(42);

 		while (la.kind == 13) {

 			Attribute(ref attrs);

 		}

 		NoUSIdent(out id);

-		if (la.kind == 15 || la.kind == 45) {

-			if (la.kind == 45) {

+		if (la.kind == 15 || la.kind == 46) {

+			if (la.kind == 46) {

 				GenericParameters(typeArgs);

 			}

 			Formals(true, true, ins, out openParen);

-			if (la.kind == 42 || la.kind == 43) {

-				if (la.kind == 42) {

+			if (la.kind == 43 || la.kind == 44) {

+				if (la.kind == 43) {

 					Get();

 				} else {

 					Get();

@@ -618,10 +654,10 @@ bool CloseOptionalBrace(bool usesOptionalBrace) {
 				}

 				Formals(false, true, outs, out openParen);

 			}

-		} else if (la.kind == 44) {

+		} else if (la.kind == 45) {

 			Get();

 			signatureEllipsis = t; openParen = Token.NoToken; 

-		} else SynErr(140);

+		} else SynErr(142);

 		while (StartOf(5)) {

 			IteratorSpec(reads, mod, decreases, req, ens, yieldReq, yieldEns, ref readsAttrs, ref modAttrs, ref decrAttrs);

 		}

@@ -648,13 +684,13 @@ bool CloseOptionalBrace(bool usesOptionalBrace) {
 		List<MemberDecl/*!*/> members = new List<MemberDecl/*!*/>();

 		IToken bodyStart;

 		

-		while (!(la.kind == 0 || la.kind == 30)) {SynErr(141); Get();}

+		while (!(la.kind == 0 || la.kind == 30)) {SynErr(143); Get();}

 		Expect(30);

 		while (la.kind == 13) {

 			Attribute(ref attrs);

 		}

 		NoUSIdent(out id);

-		if (la.kind == 45) {

+		if (la.kind == 46) {

 			GenericParameters(typeArgs);

 		}

 		Expect(13);

@@ -686,13 +722,13 @@ bool CloseOptionalBrace(bool usesOptionalBrace) {
 		}

 		if (la.kind == 36) {

 			FieldDecl(mmod, mm);

-		} else if (la.kind == 67 || la.kind == 68 || la.kind == 69) {

+		} else if (la.kind == 68 || la.kind == 69 || la.kind == 70) {

 			FunctionDecl(mmod, out f);

 			mm.Add(f); 

 		} else if (StartOf(6)) {

 			MethodDecl(mmod, allowConstructors, out m);

 			mm.Add(m); 

-		} else SynErr(142);

+		} else SynErr(144);

 	}

 

 	void Attribute(ref Attributes attrs) {

@@ -715,7 +751,7 @@ bool CloseOptionalBrace(bool usesOptionalBrace) {
 		IToken id; IToken idPrime; ids = new List<IToken>(); 

 		Ident(out id);

 		ids.Add(id); 

-		while (la.kind == 66) {

+		while (la.kind == 67) {

 			IdentOrDigitsSuffix(out id, out idPrime);

 			ids.Add(id);

 			if (idPrime != null) { ids.Add(idPrime); }

@@ -734,7 +770,7 @@ bool CloseOptionalBrace(bool usesOptionalBrace) {
 		x = Token.NoToken;

 		y = null;

 		

-		Expect(66);

+		Expect(67);

 		if (la.kind == 1) {

 			Get();

 			x = t; 

@@ -768,7 +804,7 @@ bool CloseOptionalBrace(bool usesOptionalBrace) {
 		} else if (la.kind == 11) {

 			Get();

 			x = t; 

-		} else SynErr(143);

+		} else SynErr(145);

 	}

 

 	void GenericParameters(List<TypeParameter/*!*/>/*!*/ typeArgs) {

@@ -776,12 +812,12 @@ bool CloseOptionalBrace(bool usesOptionalBrace) {
 		IToken/*!*/ id;

 		TypeParameter.EqualitySupportValue eqSupport;

 		

-		Expect(45);

+		Expect(46);

 		NoUSIdent(out id);

 		eqSupport = TypeParameter.EqualitySupportValue.Unspecified; 

 		if (la.kind == 15) {

 			Get();

-			Expect(39);

+			Expect(41);

 			Expect(16);

 			eqSupport = TypeParameter.EqualitySupportValue.Required; 

 		}

@@ -792,13 +828,13 @@ bool CloseOptionalBrace(bool usesOptionalBrace) {
 			eqSupport = TypeParameter.EqualitySupportValue.Unspecified; 

 			if (la.kind == 15) {

 				Get();

-				Expect(39);

+				Expect(41);

 				Expect(16);

 				eqSupport = TypeParameter.EqualitySupportValue.Required; 

 			}

 			typeArgs.Add(new TypeParameter(id, id.val, eqSupport)); 

 		}

-		Expect(46);

+		Expect(47);

 	}

 

 	void FieldDecl(MemberModifiers mmod, List<MemberDecl/*!*/>/*!*/ mm) {

@@ -806,7 +842,7 @@ bool CloseOptionalBrace(bool usesOptionalBrace) {
 		Attributes attrs = null;

 		IToken/*!*/ id;  Type/*!*/ ty;

 		

-		while (!(la.kind == 0 || la.kind == 36)) {SynErr(144); Get();}

+		while (!(la.kind == 0 || la.kind == 36)) {SynErr(146); Get();}

 		Expect(36);

 		if (mmod.IsStatic) { SemErr(t, "fields cannot be declared 'static'"); }

 		

@@ -820,7 +856,7 @@ bool CloseOptionalBrace(bool usesOptionalBrace) {
 			FIdentType(out id, out ty);

 			mm.Add(new Field(id, id.val, mmod.IsGhost, ty, attrs)); 

 		}

-		while (!(la.kind == 0 || la.kind == 8)) {SynErr(145); Get();}

+		while (!(la.kind == 0 || la.kind == 8)) {SynErr(147); Get();}

 		Expect(8);

 	}

 

@@ -843,9 +879,9 @@ bool CloseOptionalBrace(bool usesOptionalBrace) {
 		IToken bodyEnd = Token.NoToken;

 		IToken signatureEllipsis = null;

 		

-		if (la.kind == 67) {

+		if (la.kind == 68) {

 			Get();

-			if (la.kind == 47) {

+			if (la.kind == 48) {

 				Get();

 				isFunctionMethod = true; 

 			}

@@ -855,22 +891,22 @@ bool CloseOptionalBrace(bool usesOptionalBrace) {
 				Attribute(ref attrs);

 			}

 			NoUSIdent(out id);

-			if (la.kind == 15 || la.kind == 45) {

-				if (la.kind == 45) {

+			if (la.kind == 15 || la.kind == 46) {

+				if (la.kind == 46) {

 					GenericParameters(typeArgs);

 				}

 				Formals(true, isFunctionMethod, formals, out openParen);

 				Expect(7);

 				Type(out returnType);

-			} else if (la.kind == 44) {

+			} else if (la.kind == 45) {

 				Get();

 				signatureEllipsis = t;

 				openParen = Token.NoToken; 

-			} else SynErr(146);

-		} else if (la.kind == 68) {

+			} else SynErr(148);

+		} else if (la.kind == 69) {

 			Get();

 			isPredicate = true; 

-			if (la.kind == 47) {

+			if (la.kind == 48) {

 				Get();

 				isFunctionMethod = true; 

 			}

@@ -881,7 +917,7 @@ bool CloseOptionalBrace(bool usesOptionalBrace) {
 			}

 			NoUSIdent(out id);

 			if (StartOf(7)) {

-				if (la.kind == 45) {

+				if (la.kind == 46) {

 					GenericParameters(typeArgs);

 				}

 				if (la.kind == 15) {

@@ -891,12 +927,12 @@ bool CloseOptionalBrace(bool usesOptionalBrace) {
 						SemErr(t, "predicates do not have an explicitly declared return type; it is always bool"); 

 					}

 				}

-			} else if (la.kind == 44) {

+			} else if (la.kind == 45) {

 				Get();

 				signatureEllipsis = t;

 				openParen = Token.NoToken; 

-			} else SynErr(147);

-		} else if (la.kind == 69) {

+			} else SynErr(149);

+		} else if (la.kind == 70) {

 			Get();

 			isCoPredicate = true; 

 			if (mmod.IsGhost) { SemErr(t, "copredicates cannot be declared 'ghost' (they are ghost by default)"); }

@@ -906,7 +942,7 @@ bool CloseOptionalBrace(bool usesOptionalBrace) {
 			}

 			NoUSIdent(out id);

 			if (StartOf(7)) {

-				if (la.kind == 45) {

+				if (la.kind == 46) {

 					GenericParameters(typeArgs);

 				}

 				if (la.kind == 15) {

@@ -916,12 +952,12 @@ bool CloseOptionalBrace(bool usesOptionalBrace) {
 						SemErr(t, "copredicates do not have an explicitly declared return type; it is always bool"); 

 					}

 				}

-			} else if (la.kind == 44) {

+			} else if (la.kind == 45) {

 				Get();

 				signatureEllipsis = t;

 				openParen = Token.NoToken; 

-			} else SynErr(148);

-		} else SynErr(149);

+			} else SynErr(150);

+		} else SynErr(151);

 		decreases = isCoPredicate ? null : new List<Expression/*!*/>(); 

 		while (StartOf(8)) {

 			FunctionSpec(reqs, reads, ens, decreases);

@@ -972,21 +1008,21 @@ bool CloseOptionalBrace(bool usesOptionalBrace) {
 		IToken bodyStart = Token.NoToken;

 		IToken bodyEnd = Token.NoToken;

 		

-		while (!(StartOf(9))) {SynErr(150); Get();}

-		if (la.kind == 47) {

+		while (!(StartOf(9))) {SynErr(152); Get();}

+		if (la.kind == 48) {

 			Get();

-		} else if (la.kind == 48) {

+		} else if (la.kind == 49) {

 			Get();

 			isLemma = true; 

-		} else if (la.kind == 49) {

+		} else if (la.kind == 50) {

 			Get();

 			isCoLemma = true; 

-		} else if (la.kind == 50) {

+		} else if (la.kind == 51) {

 			Get();

 			isCoLemma = true;

 			errors.Warning(t, "the 'comethod' keyword has been deprecated; it has been renamed to 'colemma'");

 			

-		} else if (la.kind == 51) {

+		} else if (la.kind == 52) {

 			Get();

 			if (allowConstructor) {

 			 isConstructor = true;

@@ -994,7 +1030,7 @@ bool CloseOptionalBrace(bool usesOptionalBrace) {
 			 SemErr(t, "constructors are allowed only in classes");

 			}

 			

-		} else SynErr(151);

+		} else SynErr(153);

 		keywordToken = t; 

 		if (isLemma) {

 		 if (mmod.IsGhost) {

@@ -1027,20 +1063,20 @@ bool CloseOptionalBrace(bool usesOptionalBrace) {
 		 }

 		}

 		

-		if (la.kind == 15 || la.kind == 45) {

-			if (la.kind == 45) {

+		if (la.kind == 15 || la.kind == 46) {

+			if (la.kind == 46) {

 				GenericParameters(typeArgs);

 			}

 			Formals(true, !mmod.IsGhost, ins, out openParen);

-			if (la.kind == 43) {

+			if (la.kind == 44) {

 				Get();

 				if (isConstructor) { SemErr(t, "constructors cannot have out-parameters"); } 

 				Formals(false, !mmod.IsGhost, outs, out openParen);

 			}

-		} else if (la.kind == 44) {

+		} else if (la.kind == 45) {

 			Get();

 			signatureEllipsis = t; openParen = Token.NoToken; 

-		} else SynErr(152);

+		} else SynErr(154);

 		while (StartOf(10)) {

 			MethodSpec(req, mod, ens, dec, ref decAttrs, ref modAttrs);

 		}

@@ -1114,7 +1150,7 @@ bool CloseOptionalBrace(bool usesOptionalBrace) {
 		} else if (la.kind == 2) {

 			Get();

 			id = t; 

-		} else SynErr(153);

+		} else SynErr(155);

 		Expect(7);

 		Type(out ty);

 	}

@@ -1124,6 +1160,20 @@ bool CloseOptionalBrace(bool usesOptionalBrace) {
 		TypeAndToken(out tok, out ty);

 	}

 

+	void Expression(out Expression e, bool allowSemi, bool allowLambda) {

+		Expression e0; IToken endTok; 

+		EquivExpression(out e, allowSemi, allowLambda);

+		if (SemiFollowsCall(allowSemi, e)) {

+			Expect(8);

+			endTok = t; 

+			Expression(out e0, allowSemi, allowLambda);

+			e = new StmtExpr(e.tok,

+			     new UpdateStmt(e.tok, endTok, new List<Expression>(), new List<AssignmentRhs>() { new ExprRhs(e, null) }),

+			     e0);

+			

+		}

+	}

+

 	void GIdentType(bool allowGhostKeyword, out IToken/*!*/ id, out Type/*!*/ ty, out bool isGhost) {

 		Contract.Ensures(Contract.ValueAtReturn(out id)!=null);

 		Contract.Ensures(Contract.ValueAtReturn(out ty)!=null);

@@ -1184,7 +1234,7 @@ bool CloseOptionalBrace(bool usesOptionalBrace) {
 			Get();

 			isGhost = true; 

 		}

-		if (StartOf(4)) {

+		if (StartOf(3)) {

 			TypeAndToken(out id, out ty);

 			if (la.kind == 7) {

 				Get();

@@ -1202,7 +1252,7 @@ bool CloseOptionalBrace(bool usesOptionalBrace) {
 			id = t; name = id.val;

 			Expect(7);

 			Type(out ty);

-		} else SynErr(154);

+		} else SynErr(156);

 		if (name != null) {

 		 identName = name;

 		} else {

@@ -1217,30 +1267,30 @@ bool CloseOptionalBrace(bool usesOptionalBrace) {
 		List<Type> gt = null;

 		

 		switch (la.kind) {

-		case 57: {

+		case 58: {

 			Get();

 			tok = t; 

 			break;

 		}

-		case 58: {

+		case 59: {

 			Get();

 			tok = t;  ty = new NatType(); 

 			break;

 		}

-		case 59: {

+		case 60: {

 			Get();

 			tok = t;  ty = new IntType(); 

 			break;

 		}

-		case 60: {

+		case 61: {

 			Get();

 			tok = t;  ty = new RealType(); 

 			break;

 		}

-		case 61: {

+		case 62: {

 			Get();

 			tok = t;  gt = new List<Type/*!*/>(); 

-			if (la.kind == 45) {

+			if (la.kind == 46) {

 				GenericInstantiation(gt);

 			}

 			if (gt.Count > 1) {

@@ -1250,10 +1300,10 @@ bool CloseOptionalBrace(bool usesOptionalBrace) {
 			

 			break;

 		}

-		case 62: {

+		case 63: {

 			Get();

 			tok = t;  gt = new List<Type/*!*/>(); 

-			if (la.kind == 45) {

+			if (la.kind == 46) {

 				GenericInstantiation(gt);

 			}

 			if (gt.Count > 1) {

@@ -1263,10 +1313,10 @@ bool CloseOptionalBrace(bool usesOptionalBrace) {
 			

 			break;

 		}

-		case 63: {

+		case 64: {

 			Get();

 			tok = t;  gt = new List<Type/*!*/>(); 

-			if (la.kind == 45) {

+			if (la.kind == 46) {

 				GenericInstantiation(gt);

 			}

 			if (gt.Count > 1) {

@@ -1276,10 +1326,10 @@ bool CloseOptionalBrace(bool usesOptionalBrace) {
 			

 			break;

 		}

-		case 64: {

+		case 65: {

 			Get();

 			tok = t;  gt = new List<Type/*!*/>(); 

-			if (la.kind == 45) {

+			if (la.kind == 46) {

 				GenericInstantiation(gt);

 			}

 			if (gt.Count == 0) {

@@ -1296,7 +1346,7 @@ bool CloseOptionalBrace(bool usesOptionalBrace) {
 		case 15: {

 			Get();

 			tok = t; gt = new List<Type>(); 

-			if (StartOf(4)) {

+			if (StartOf(3)) {

 				Type(out ty);

 				gt.Add(ty); 

 				while (la.kind == 37) {

@@ -1317,11 +1367,11 @@ bool CloseOptionalBrace(bool usesOptionalBrace) {
 			

 			break;

 		}

-		case 1: case 5: case 65: {

+		case 1: case 5: case 66: {

 			ReferenceType(out tok, out ty);

 			break;

 		}

-		default: SynErr(155); break;

+		default: SynErr(157); break;

 		}

 		if (la.kind == 10) {

 			Type t2; 

@@ -1357,7 +1407,7 @@ List<MaybeFreeExpression/*!*/>/*!*/ yieldReq, List<MaybeFreeExpression/*!*/>/*!*
 ref Attributes readsAttrs, ref Attributes modAttrs, ref Attributes decrAttrs) {

 		Expression/*!*/ e; FrameExpression/*!*/ fe; bool isFree = false; bool isYield = false; Attributes ensAttrs = null;

 		

-		while (!(StartOf(12))) {SynErr(156); Get();}

+		while (!(StartOf(12))) {SynErr(158); Get();}

 		if (la.kind == 11) {

 			Get();

 			while (IsAttribute()) {

@@ -1372,9 +1422,9 @@ ref Attributes readsAttrs, ref Attributes modAttrs, ref Attributes decrAttrs) {
 					reads.Add(fe); 

 				}

 			}

-			while (!(la.kind == 0 || la.kind == 8)) {SynErr(157); Get();}

+			while (!(la.kind == 0 || la.kind == 8)) {SynErr(159); Get();}

 			Expect(8);

-		} else if (la.kind == 52) {

+		} else if (la.kind == 53) {

 			Get();

 			while (IsAttribute()) {

 				Attribute(ref modAttrs);

@@ -1388,21 +1438,21 @@ ref Attributes readsAttrs, ref Attributes modAttrs, ref Attributes decrAttrs) {
 					mod.Add(fe); 

 				}

 			}

-			while (!(la.kind == 0 || la.kind == 8)) {SynErr(158); Get();}

+			while (!(la.kind == 0 || la.kind == 8)) {SynErr(160); Get();}

 			Expect(8);

 		} else if (StartOf(14)) {

-			if (la.kind == 53) {

+			if (la.kind == 54) {

 				Get();

 				isFree = true; 

 			}

-			if (la.kind == 56) {

+			if (la.kind == 57) {

 				Get();

 				isYield = true; 

 			}

 			if (la.kind == 12) {

 				Get();

 				Expression(out e, false, true);

-				while (!(la.kind == 0 || la.kind == 8)) {SynErr(159); Get();}

+				while (!(la.kind == 0 || la.kind == 8)) {SynErr(161); Get();}

 				Expect(8);

 				if (isYield) {

 				yieldReq.Add(new MaybeFreeExpression(e, isFree));

@@ -1410,13 +1460,13 @@ ref Attributes readsAttrs, ref Attributes modAttrs, ref Attributes decrAttrs) {
 				req.Add(new MaybeFreeExpression(e, isFree));

 				}

 				

-			} else if (la.kind == 54) {

+			} else if (la.kind == 55) {

 				Get();

 				while (IsAttribute()) {

 					Attribute(ref ensAttrs);

 				}

 				Expression(out e, false, true);

-				while (!(la.kind == 0 || la.kind == 8)) {SynErr(160); Get();}

+				while (!(la.kind == 0 || la.kind == 8)) {SynErr(162); Get();}

 				Expect(8);

 				if (isYield) {

 				yieldEns.Add(new MaybeFreeExpression(e, isFree, ensAttrs));

@@ -1424,16 +1474,16 @@ ref Attributes readsAttrs, ref Attributes modAttrs, ref Attributes decrAttrs) {
 				ens.Add(new MaybeFreeExpression(e, isFree, ensAttrs));

 				}

 				

-			} else SynErr(161);

-		} else if (la.kind == 55) {

+			} else SynErr(163);

+		} else if (la.kind == 56) {

 			Get();

 			while (IsAttribute()) {

 				Attribute(ref decrAttrs);

 			}

 			DecreasesList(decreases, false);

-			while (!(la.kind == 0 || la.kind == 8)) {SynErr(162); Get();}

+			while (!(la.kind == 0 || la.kind == 8)) {SynErr(164); Get();}

 			Expect(8);

-		} else SynErr(163);

+		} else SynErr(165);

 	}

 

 	void BlockStmt(out BlockStmt/*!*/ block, out IToken bodyStart, out IToken bodyEnd) {

@@ -1455,8 +1505,8 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 		Contract.Requires(cce.NonNullElements(req)); Contract.Requires(cce.NonNullElements(mod)); Contract.Requires(cce.NonNullElements(ens)); Contract.Requires(cce.NonNullElements(decreases));

 		Expression/*!*/ e;  FrameExpression/*!*/ fe;  bool isFree = false; Attributes ensAttrs = null;

 		

-		while (!(StartOf(16))) {SynErr(164); Get();}

-		if (la.kind == 52) {

+		while (!(StartOf(16))) {SynErr(166); Get();}

+		if (la.kind == 53) {

 			Get();

 			while (IsAttribute()) {

 				Attribute(ref modAttrs);

@@ -1470,38 +1520,38 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 					mod.Add(fe); 

 				}

 			}

-			while (!(la.kind == 0 || la.kind == 8)) {SynErr(165); Get();}

+			while (!(la.kind == 0 || la.kind == 8)) {SynErr(167); Get();}

 			Expect(8);

-		} else if (la.kind == 12 || la.kind == 53 || la.kind == 54) {

-			if (la.kind == 53) {

+		} else if (la.kind == 12 || la.kind == 54 || la.kind == 55) {

+			if (la.kind == 54) {

 				Get();

 				isFree = true; 

 			}

 			if (la.kind == 12) {

 				Get();

 				Expression(out e, false, true);

-				while (!(la.kind == 0 || la.kind == 8)) {SynErr(166); Get();}

+				while (!(la.kind == 0 || la.kind == 8)) {SynErr(168); Get();}

 				Expect(8);

 				req.Add(new MaybeFreeExpression(e, isFree)); 

-			} else if (la.kind == 54) {

+			} else if (la.kind == 55) {

 				Get();

 				while (IsAttribute()) {

 					Attribute(ref ensAttrs);

 				}

 				Expression(out e, false, true);

-				while (!(la.kind == 0 || la.kind == 8)) {SynErr(167); Get();}

+				while (!(la.kind == 0 || la.kind == 8)) {SynErr(169); Get();}

 				Expect(8);

 				ens.Add(new MaybeFreeExpression(e, isFree, ensAttrs)); 

-			} else SynErr(168);

-		} else if (la.kind == 55) {

+			} else SynErr(170);

+		} else if (la.kind == 56) {

 			Get();

 			while (IsAttribute()) {

 				Attribute(ref decAttrs);

 			}

 			DecreasesList(decreases, true);

-			while (!(la.kind == 0 || la.kind == 8)) {SynErr(169); Get();}

+			while (!(la.kind == 0 || la.kind == 8)) {SynErr(171); Get();}

 			Expect(8);

-		} else SynErr(170);

+		} else SynErr(172);

 	}

 

 	void FrameExpression(out FrameExpression/*!*/ fe) {

@@ -1514,32 +1564,18 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 		if (StartOf(17)) {

 			Expression(out e, false, false);

 			feTok = e.tok; 

-			if (la.kind == 70) {

+			if (la.kind == 71) {

 				Get();

 				Ident(out id);

 				fieldName = id.val;  feTok = id; 

 			}

 			fe = new FrameExpression(feTok, e, fieldName); 

-		} else if (la.kind == 70) {

+		} else if (la.kind == 71) {

 			Get();

 			Ident(out id);

 			fieldName = id.val; 

 			fe = new FrameExpression(id, new ImplicitThisExpr(id), fieldName); 

-		} else SynErr(171);

-	}

-

-	void Expression(out Expression e, bool allowSemi, bool allowLambda) {

-		Expression e0; IToken endTok; 

-		EquivExpression(out e, allowSemi, allowLambda);

-		if (SemiFollowsCall(allowSemi, e)) {

-			Expect(8);

-			endTok = t; 

-			Expression(out e0, allowSemi, allowLambda);

-			e = new StmtExpr(e.tok,

-			     new UpdateStmt(e.tok, endTok, new List<Expression>(), new List<AssignmentRhs>() { new ExprRhs(e, null) }),

-			     e0);

-			

-		}

+		} else SynErr(173);

 	}

 

 	void DecreasesList(List<Expression/*!*/> decreases, bool allowWildcard) {

@@ -1565,7 +1601,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 

 	void GenericInstantiation(List<Type/*!*/>/*!*/ gt) {

 		Contract.Requires(cce.NonNullElements(gt)); Type/*!*/ ty; 

-		Expect(45);

+		Expect(46);

 		Type(out ty);

 		gt.Add(ty); 

 		while (la.kind == 37) {

@@ -1573,7 +1609,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 			Type(out ty);

 			gt.Add(ty); 

 		}

-		Expect(46);

+		Expect(47);

 	}

 

 	void ReferenceType(out IToken/*!*/ tok, out Type/*!*/ ty) {

@@ -1582,13 +1618,13 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 		List<Type> gt;

 		List<IToken> path;

 		

-		if (la.kind == 65) {

+		if (la.kind == 66) {

 			Get();

 			tok = t;  ty = new ObjectType(); 

 		} else if (la.kind == 5) {

 			Get();

 			tok = t;  gt = new List<Type>(); 

-			if (la.kind == 45) {

+			if (la.kind == 46) {

 				GenericInstantiation(gt);

 			}

 			int dims = tok.val.Length == 5 ? 1 : int.Parse(tok.val.Substring(5));

@@ -1598,16 +1634,16 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 			Ident(out tok);

 			gt = new List<Type>();

 			path = new List<IToken>(); 

-			while (la.kind == 66) {

+			while (la.kind == 67) {

 				path.Add(tok); 

 				Get();

 				Ident(out tok);

 			}

-			if (la.kind == 45) {

+			if (la.kind == 46) {

 				GenericInstantiation(gt);

 			}

 			ty = new UserDefinedType(tok, tok.val, gt, path); 

-		} else SynErr(172);

+		} else SynErr(174);

 	}

 

 	void FunctionSpec(List<Expression/*!*/>/*!*/ reqs, List<FrameExpression/*!*/>/*!*/ reads, List<Expression/*!*/>/*!*/ ens, List<Expression/*!*/> decreases) {

@@ -1616,10 +1652,10 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 		Contract.Requires(decreases == null || cce.NonNullElements(decreases));

 		Expression/*!*/ e;  FrameExpression/*!*/ fe; 

 		if (la.kind == 12) {

-			while (!(la.kind == 0 || la.kind == 12)) {SynErr(173); Get();}

+			while (!(la.kind == 0 || la.kind == 12)) {SynErr(175); Get();}

 			Get();

 			Expression(out e, false, true);

-			while (!(la.kind == 0 || la.kind == 8)) {SynErr(174); Get();}

+			while (!(la.kind == 0 || la.kind == 8)) {SynErr(176); Get();}

 			Expect(8);

 			reqs.Add(e); 

 		} else if (la.kind == 11) {

@@ -1633,15 +1669,15 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 					reads.Add(fe); 

 				}

 			}

-			while (!(la.kind == 0 || la.kind == 8)) {SynErr(175); Get();}

+			while (!(la.kind == 0 || la.kind == 8)) {SynErr(177); Get();}

 			Expect(8);

-		} else if (la.kind == 54) {

+		} else if (la.kind == 55) {

 			Get();

 			Expression(out e, false, true);

-			while (!(la.kind == 0 || la.kind == 8)) {SynErr(176); Get();}

+			while (!(la.kind == 0 || la.kind == 8)) {SynErr(178); Get();}

 			Expect(8);

 			ens.Add(e); 

-		} else if (la.kind == 55) {

+		} else if (la.kind == 56) {

 			Get();

 			if (decreases == null) {

 			 SemErr(t, "'decreases' clauses are meaningless for copredicates, so they are not allowed");

@@ -1649,9 +1685,9 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 			}

 			

 			DecreasesList(decreases, false);

-			while (!(la.kind == 0 || la.kind == 8)) {SynErr(177); Get();}

+			while (!(la.kind == 0 || la.kind == 8)) {SynErr(179); Get();}

 			Expect(8);

-		} else SynErr(178);

+		} else SynErr(180);

 	}

 

 	void FunctionBody(out Expression/*!*/ e, out IToken bodyStart, out IToken bodyEnd) {

@@ -1670,7 +1706,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 			fe = new FrameExpression(t, new WildcardExpr(t), null); 

 		} else if (StartOf(13)) {

 			FrameExpression(out fe);

-		} else SynErr(179);

+		} else SynErr(181);

 	}

 

 	void LambdaSpec(out Expression req, List<FrameExpression> reads) {

@@ -1702,7 +1738,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 			e = new WildcardExpr(t); 

 		} else if (StartOf(17)) {

 			Expression(out e, false, false);

-		} else SynErr(180);

+		} else SynErr(182);

 	}

 

 	void Stmt(List<Statement/*!*/>/*!*/ ss) {

@@ -1719,14 +1755,14 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 		IToken bodyStart, bodyEnd;

 		int breakCount;

 		

-		while (!(StartOf(19))) {SynErr(181); Get();}

+		while (!(StartOf(19))) {SynErr(183); Get();}

 		switch (la.kind) {

 		case 13: {

 			BlockStmt(out bs, out bodyStart, out bodyEnd);

 			s = bs; 

 			break;

 		}

-		case 86: {

+		case 87: {

 			AssertStmt(out s);

 			break;

 		}

@@ -1734,11 +1770,11 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 			AssumeStmt(out s);

 			break;

 		}

-		case 87: {

+		case 88: {

 			PrintStmt(out s);

 			break;

 		}

-		case 1: case 2: case 3: case 4: case 15: case 35: case 59: case 60: case 116: case 117: case 118: case 119: case 120: case 121: {

+		case 1: case 2: case 3: case 4: case 15: case 35: case 60: case 61: case 117: case 118: case 119: case 120: case 121: case 122: {

 			UpdateStmt(out s);

 			break;

 		}

@@ -1746,31 +1782,31 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 			VarDeclStatement(out s);

 			break;

 		}

-		case 80: {

+		case 81: {

 			IfStmt(out s);

 			break;

 		}

-		case 83: {

+		case 84: {

 			WhileStmt(out s);

 			break;

 		}

-		case 85: {

+		case 86: {

 			MatchStmt(out s);

 			break;

 		}

-		case 88: case 89: {

+		case 89: case 90: {

 			ForallStmt(out s);

 			break;

 		}

-		case 91: {

+		case 92: {

 			CalcStmt(out s);

 			break;

 		}

-		case 90: {

+		case 91: {

 			ModifyStmt(out s);

 			break;

 		}

-		case 71: {

+		case 72: {

 			Get();

 			x = t; 

 			NoUSIdent(out id);

@@ -1779,32 +1815,32 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 			s.Labels = new LList<Label>(new Label(x, id.val), s.Labels); 

 			break;

 		}

-		case 72: {

+		case 73: {

 			Get();

 			x = t; breakCount = 1; label = null; 

 			if (la.kind == 1) {

 				NoUSIdent(out id);

 				label = id.val; 

-			} else if (la.kind == 8 || la.kind == 72) {

-				while (la.kind == 72) {

+			} else if (la.kind == 8 || la.kind == 73) {

+				while (la.kind == 73) {

 					Get();

 					breakCount++; 

 				}

-			} else SynErr(182);

-			while (!(la.kind == 0 || la.kind == 8)) {SynErr(183); Get();}

+			} else SynErr(184);

+			while (!(la.kind == 0 || la.kind == 8)) {SynErr(185); Get();}

 			Expect(8);

 			s = label != null ? new BreakStmt(x, t, label) : new BreakStmt(x, t, breakCount); 

 			break;

 		}

-		case 56: case 75: {

+		case 57: case 75: {

 			ReturnStmt(out s);

 			break;

 		}

-		case 44: {

+		case 45: {

 			SkeletonStmt(out s);

 			break;

 		}

-		default: SynErr(184); break;

+		default: SynErr(186); break;

 		}

 	}

 

@@ -1813,17 +1849,17 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 		Expression e = dummyExpr; Attributes attrs = null;

 		IToken dotdotdot = null;

 		

-		Expect(86);

+		Expect(87);

 		x = t; 

 		while (IsAttribute()) {

 			Attribute(ref attrs);

 		}

 		if (StartOf(17)) {

 			Expression(out e, false, true);

-		} else if (la.kind == 44) {

+		} else if (la.kind == 45) {

 			Get();

 			dotdotdot = t; 

-		} else SynErr(185);

+		} else SynErr(187);

 		Expect(8);

 		if (dotdotdot != null) {

 		 s = new SkeletonStatement(new AssertStmt(x, t, new LiteralExpr(x, true), attrs), dotdotdot, null);

@@ -1845,10 +1881,10 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 		}

 		if (StartOf(17)) {

 			Expression(out e, false, true);

-		} else if (la.kind == 44) {

+		} else if (la.kind == 45) {

 			Get();

 			dotdotdot = t; 

-		} else SynErr(186);

+		} else SynErr(188);

 		Expect(8);

 		if (dotdotdot != null) {

 		 s = new SkeletonStatement(new AssumeStmt(x, t, new LiteralExpr(x, true), attrs), dotdotdot, null);

@@ -1862,7 +1898,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 		Contract.Ensures(Contract.ValueAtReturn(out s) != null); IToken/*!*/ x;  Attributes.Argument/*!*/ arg;

 		List<Attributes.Argument/*!*/> args = new List<Attributes.Argument/*!*/>();

 		

-		Expect(87);

+		Expect(88);

 		x = t; 

 		AttributeArg(out arg, false);

 		args.Add(arg); 

@@ -1918,13 +1954,13 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 					suchThatAssume = t; 

 				}

 				Expression(out suchThat, false, true);

-			} else SynErr(187);

+			} else SynErr(189);

 			Expect(8);

 			endTok = t; 

 		} else if (la.kind == 7) {

 			Get();

 			SemErr(t, "invalid statement (did you forget the 'label' keyword?)"); 

-		} else SynErr(188);

+		} else SynErr(190);

 		if (suchThat != null) {

 		 s = new AssignSuchThatStmt(x, endTok, lhss, suchThat, suchThatAssume);

 		} else {

@@ -2023,7 +2059,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 		List<GuardedAlternative> alternatives;

 		ifStmt = dummyStmt;  // to please the compiler

 		

-		Expect(80);

+		Expect(81);

 		x = t; 

 		if (IsAlternative()) {

 			AlternativeBlock(out alternatives, out endTok);

@@ -2037,15 +2073,15 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 			}

 			BlockStmt(out thn, out bodyStart, out bodyEnd);

 			endTok = thn.EndTok; 

-			if (la.kind == 81) {

+			if (la.kind == 82) {

 				Get();

-				if (la.kind == 80) {

+				if (la.kind == 81) {

 					IfStmt(out s);

 					els = s; endTok = s.EndTok; 

 				} else if (la.kind == 13) {

 					BlockStmt(out bs, out bodyStart, out bodyEnd);

 					els = bs; endTok = bs.EndTok; 

-				} else SynErr(189);

+				} else SynErr(191);

 			}

 			if (guardEllipsis != null) {

 			 ifStmt = new SkeletonStatement(new IfStmt(x, endTok, guard, thn, els), guardEllipsis, null);

@@ -2053,7 +2089,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 			 ifStmt = new IfStmt(x, endTok, guard, thn, els);

 			}

 			

-		} else SynErr(190);

+		} else SynErr(192);

 	}

 

 	void WhileStmt(out Statement/*!*/ stmt) {

@@ -2069,7 +2105,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 		List<GuardedAlternative> alternatives;

 		stmt = dummyStmt;  // to please the compiler

 		

-		Expect(83);

+		Expect(84);

 		x = t; 

 		if (IsLoopSpecOrAlternative()) {

 			LoopSpec(out invariants, out decreases, out mod, ref decAttrs, ref modAttrs);

@@ -2087,10 +2123,10 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 			if (la.kind == 13) {

 				BlockStmt(out body, out bodyStart, out bodyEnd);

 				endTok = body.EndTok; 

-			} else if (la.kind == 44) {

+			} else if (la.kind == 45) {

 				Get();

 				bodyEllipsis = t; endTok = t; 

-			} else SynErr(191);

+			} else SynErr(193);

 			if (guardEllipsis != null || bodyEllipsis != null) {

 			 if (mod != null) {

 			   SemErr(mod[0].E.tok, "'modifies' clauses are not allowed on refining loops");

@@ -2106,7 +2142,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 			 stmt = new WhileStmt(x, endTok, guard, invariants, new Specification<Expression>(decreases, decAttrs), new Specification<FrameExpression>(mod, modAttrs), body);

 			}

 			

-		} else SynErr(192);

+		} else SynErr(194);

 	}

 

 	void MatchStmt(out Statement/*!*/ s) {

@@ -2115,14 +2151,14 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 		List<MatchCaseStmt/*!*/> cases = new List<MatchCaseStmt/*!*/>();

 		bool usesOptionalBrace = false;

 		

-		Expect(85);

+		Expect(86);

 		x = t; 

 		Expression(out e, true, true);

 		if (la.kind == 13) {

 			Get();

 			usesOptionalBrace = true; 

 		}

-		while (la.kind == 82) {

+		while (la.kind == 83) {

 			CaseStatement(out c);

 			cases.Add(c); 

 		}

@@ -2130,7 +2166,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 			Expect(14);

 		} else if (StartOf(22)) {

 			if (usesOptionalBrace) { SemErr(t, "expecting close curly brace"); } 

-		} else SynErr(193);

+		} else SynErr(195);

 		s = new MatchStmt(x, t, e, cases, usesOptionalBrace); 

 	}

 

@@ -2148,15 +2184,15 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 		IToken bodyStart, bodyEnd;

 		IToken tok = Token.NoToken;

 		

-		if (la.kind == 88) {

+		if (la.kind == 89) {

 			Get();

 			x = t; tok = x; 

-		} else if (la.kind == 89) {

+		} else if (la.kind == 90) {

 			Get();

 			x = t;

 			errors.Warning(t, "the 'parallel' keyword has been deprecated; the comprehension statement now uses the keyword 'forall' (and the parentheses around the bound variables are now optional)");

 			

-		} else SynErr(194);

+		} else SynErr(196);

 		if (la.kind == 15) {

 			Get();

 			usesOptionalParen = true; 

@@ -2174,14 +2210,14 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 			Expect(16);

 		} else if (StartOf(23)) {

 			if (usesOptionalParen) { SemErr(t, "expecting close parenthesis"); } 

-		} else SynErr(195);

-		while (la.kind == 53 || la.kind == 54) {

+		} else SynErr(197);

+		while (la.kind == 54 || la.kind == 55) {

 			isFree = false; 

-			if (la.kind == 53) {

+			if (la.kind == 54) {

 				Get();

 				isFree = true; 

 			}

-			Expect(54);

+			Expect(55);

 			Expression(out e, false, true);

 			ens.Add(new MaybeFreeExpression(e, isFree)); 

 			Expect(8);

@@ -2215,7 +2251,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 		IToken opTok;

 		IToken danglingOperator = null;

 		

-		Expect(91);

+		Expect(92);

 		x = t; 

 		if (StartOf(24)) {

 			CalcOp(out opTok, out calcOp);

@@ -2268,7 +2304,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 		BlockStmt body = null;  IToken bodyStart;

 		IToken ellipsisToken = null;

 		

-		Expect(90);

+		Expect(91);

 		tok = t; 

 		while (IsAttribute()) {

 			Attribute(ref attrs);

@@ -2290,10 +2326,10 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 		if (la.kind == 13) {

 			BlockStmt(out body, out bodyStart, out endTok);

 		} else if (la.kind == 8) {

-			while (!(la.kind == 0 || la.kind == 8)) {SynErr(196); Get();}

+			while (!(la.kind == 0 || la.kind == 8)) {SynErr(198); Get();}

 			Get();

 			endTok = t; 

-		} else SynErr(197);

+		} else SynErr(199);

 		s = new ModifyStmt(tok, endTok, mod, attrs, body);

 		if (ellipsisToken != null) {

 		 s = new SkeletonStatement(s, ellipsisToken, null);

@@ -2310,10 +2346,10 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 		if (la.kind == 75) {

 			Get();

 			returnTok = t; 

-		} else if (la.kind == 56) {

+		} else if (la.kind == 57) {

 			Get();

 			returnTok = t; isYield = true; 

-		} else SynErr(198);

+		} else SynErr(200);

 		if (StartOf(26)) {

 			Rhs(out r, null);

 			rhss = new List<AssignmentRhs>(); rhss.Add(r); 

@@ -2337,9 +2373,9 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 		List<Expression> exprs = null;

 		IToken tok, dotdotdot, whereTok;

 		Expression e; 

-		Expect(44);

+		Expect(45);

 		dotdotdot = t; 

-		if (la.kind == 73) {

+		if (la.kind == 39) {

 			Get();

 			names = new List<IToken>(); exprs = new List<Expression>(); whereTok = t;

 			Ident(out tok);

@@ -2376,21 +2412,21 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 		r = dummyRhs;  // to please compiler

 		Attributes attrs = null;

 		

-		if (la.kind == 40) {

+		if (la.kind == 78) {

 			Get();

 			newToken = t; 

 			TypeAndToken(out x, out ty);

-			if (la.kind == 15 || la.kind == 66 || la.kind == 78) {

-				if (la.kind == 78) {

+			if (la.kind == 15 || la.kind == 67 || la.kind == 79) {

+				if (la.kind == 79) {

 					Get();

 					ee = new List<Expression>(); 

 					Expressions(ee);

-					Expect(79);

+					Expect(80);

 					var tmp = theBuiltIns.ArrayType(ee.Count, new IntType(), true);

 					

 				} else {

 					x = null; args = new List<Expression/*!*/>(); 

-					if (la.kind == 66) {

+					if (la.kind == 67) {

 						Get();

 						Ident(out x);

 					}

@@ -2415,7 +2451,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 		} else if (StartOf(17)) {

 			Expression(out e, false, true);

 			r = new ExprRhs(e); 

-		} else SynErr(199);

+		} else SynErr(201);

 		while (la.kind == 13) {

 			Attribute(ref attrs);

 		}

@@ -2427,17 +2463,17 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 		

 		if (la.kind == 1) {

 			DottedIdentifiersAndFunction(out e, false, false);

-			while (la.kind == 66 || la.kind == 78) {

+			while (la.kind == 67 || la.kind == 79) {

 				Suffix(ref e);

 			}

 			ApplySuffix(ref e);

 		} else if (StartOf(27)) {

 			ConstAtomExpression(out e, false, false);

 			Suffix(ref e);

-			while (la.kind == 66 || la.kind == 78) {

+			while (la.kind == 67 || la.kind == 79) {

 				Suffix(ref e);

 			}

-		} else SynErr(200);

+		} else SynErr(202);

 	}

 

 	void Expressions(List<Expression/*!*/>/*!*/ args) {

@@ -2458,7 +2494,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 		List<Statement> body;

 		

 		Expect(13);

-		while (la.kind == 82) {

+		while (la.kind == 83) {

 			Get();

 			x = t; 

 			Expression(out e, true, false);

@@ -2486,7 +2522,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 		} else if (StartOf(17)) {

 			Expression(out ee, true, true);

 			e = ee; 

-		} else SynErr(201);

+		} else SynErr(203);

 	}

 

 	void LoopSpec(out List<MaybeFreeExpression/*!*/> invariants, out List<Expression/*!*/> decreases, out List<FrameExpression/*!*/> mod, ref Attributes decAttrs, ref Attributes modAttrs) {

@@ -2497,22 +2533,22 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 		mod = null;

 		

 		while (StartOf(28)) {

-			if (la.kind == 53 || la.kind == 84) {

+			if (la.kind == 54 || la.kind == 85) {

 				Invariant(out invariant);

-				while (!(la.kind == 0 || la.kind == 8)) {SynErr(202); Get();}

+				while (!(la.kind == 0 || la.kind == 8)) {SynErr(204); Get();}

 				Expect(8);

 				invariants.Add(invariant); 

-			} else if (la.kind == 55) {

-				while (!(la.kind == 0 || la.kind == 55)) {SynErr(203); Get();}

+			} else if (la.kind == 56) {

+				while (!(la.kind == 0 || la.kind == 56)) {SynErr(205); Get();}

 				Get();

 				while (IsAttribute()) {

 					Attribute(ref decAttrs);

 				}

 				DecreasesList(decreases, true);

-				while (!(la.kind == 0 || la.kind == 8)) {SynErr(204); Get();}

+				while (!(la.kind == 0 || la.kind == 8)) {SynErr(206); Get();}

 				Expect(8);

 			} else {

-				while (!(la.kind == 0 || la.kind == 52)) {SynErr(205); Get();}

+				while (!(la.kind == 0 || la.kind == 53)) {SynErr(207); Get();}

 				Get();

 				while (IsAttribute()) {

 					Attribute(ref modAttrs);

@@ -2527,7 +2563,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 						mod.Add(fe); 

 					}

 				}

-				while (!(la.kind == 0 || la.kind == 8)) {SynErr(206); Get();}

+				while (!(la.kind == 0 || la.kind == 8)) {SynErr(208); Get();}

 				Expect(8);

 			}

 		}

@@ -2535,12 +2571,12 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 

 	void Invariant(out MaybeFreeExpression/*!*/ invariant) {

 		bool isFree = false; Expression/*!*/ e; List<string> ids = new List<string>(); invariant = null; Attributes attrs = null; 

-		while (!(la.kind == 0 || la.kind == 53 || la.kind == 84)) {SynErr(207); Get();}

-		if (la.kind == 53) {

+		while (!(la.kind == 0 || la.kind == 54 || la.kind == 85)) {SynErr(209); Get();}

+		if (la.kind == 54) {

 			Get();

 			isFree = true; 

 		}

-		Expect(84);

+		Expect(85);

 		while (IsAttribute()) {

 			Attribute(ref attrs);

 		}

@@ -2555,7 +2591,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 		BoundVar/*!*/ bv;

 		List<Statement/*!*/> body = new List<Statement/*!*/>();

 		

-		Expect(82);

+		Expect(83);

 		x = t; 

 		Ident(out id);

 		if (la.kind == 15) {

@@ -2584,7 +2620,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 		} else if (StartOf(17)) {

 			Expression(out e, allowSemi, true);

 			arg = new Attributes.Argument(t, e); 

-		} else SynErr(208);

+		} else SynErr(210);

 	}

 

 	void QuantifierDomain(out List<BoundVar> bvars, out Attributes attrs, out Expression range) {

@@ -2615,73 +2651,73 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 		x = null;

 		

 		switch (la.kind) {

-		case 39: {

+		case 41: {

 			Get();

 			x = t;  binOp = BinaryExpr.Opcode.Eq; 

-			if (la.kind == 92) {

+			if (la.kind == 93) {

 				Get();

-				Expect(78);

-				Expression(out k, true, true);

 				Expect(79);

+				Expression(out k, true, true);

+				Expect(80);

 			}

 			break;

 		}

-		case 45: {

+		case 46: {

 			Get();

 			x = t;  binOp = BinaryExpr.Opcode.Lt; 

 			break;

 		}

-		case 46: {

+		case 47: {

 			Get();

 			x = t;  binOp = BinaryExpr.Opcode.Gt; 

 			break;

 		}

-		case 93: {

+		case 94: {

 			Get();

 			x = t;  binOp = BinaryExpr.Opcode.Le; 

 			break;

 		}

-		case 94: {

+		case 95: {

 			Get();

 			x = t;  binOp = BinaryExpr.Opcode.Ge; 

 			break;

 		}

-		case 95: {

+		case 96: {

 			Get();

 			x = t;  binOp = BinaryExpr.Opcode.Neq; 

 			break;

 		}

-		case 96: {

+		case 97: {

 			Get();

 			x = t;  binOp = BinaryExpr.Opcode.Neq; 

 			break;

 		}

-		case 97: {

+		case 98: {

 			Get();

 			x = t;  binOp = BinaryExpr.Opcode.Le; 

 			break;

 		}

-		case 98: {

+		case 99: {

 			Get();

 			x = t;  binOp = BinaryExpr.Opcode.Ge; 

 			break;

 		}

-		case 99: case 100: {

+		case 100: case 101: {

 			EquivOp();

 			x = t;  binOp = BinaryExpr.Opcode.Iff; 

 			break;

 		}

-		case 101: case 102: {

+		case 102: case 103: {

 			ImpliesOp();

 			x = t;  binOp = BinaryExpr.Opcode.Imp; 

 			break;

 		}

-		case 103: case 104: {

+		case 104: case 105: {

 			ExpliesOp();

 			x = t;  binOp = BinaryExpr.Opcode.Exp; 

 			break;

 		}

-		default: SynErr(209); break;

+		default: SynErr(211); break;

 		}

 		if (k == null) {

 		 op = new Microsoft.Dafny.CalcStmt.BinaryCalcOp(binOp);

@@ -2700,7 +2736,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 		Token x = la;

 		IToken endTok = x;

 		

-		while (la.kind == 13 || la.kind == 91) {

+		while (la.kind == 13 || la.kind == 92) {

 			if (la.kind == 13) {

 				BlockStmt(out block, out bodyStart, out bodyEnd);

 				endTok = block.EndTok; subhints.Add(block); 

@@ -2714,33 +2750,33 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 	}

 

 	void EquivOp() {

-		if (la.kind == 99) {

+		if (la.kind == 100) {

 			Get();

-		} else if (la.kind == 100) {

+		} else if (la.kind == 101) {

 			Get();

-		} else SynErr(210);

+		} else SynErr(212);

 	}

 

 	void ImpliesOp() {

-		if (la.kind == 101) {

+		if (la.kind == 102) {

 			Get();

-		} else if (la.kind == 102) {

+		} else if (la.kind == 103) {

 			Get();

-		} else SynErr(211);

+		} else SynErr(213);

 	}

 

 	void ExpliesOp() {

-		if (la.kind == 103) {

+		if (la.kind == 104) {

 			Get();

-		} else if (la.kind == 104) {

+		} else if (la.kind == 105) {

 			Get();

-		} else SynErr(212);

+		} else SynErr(214);

 	}

 

 	void EquivExpression(out Expression e0, bool allowSemi, bool allowLambda) {

 		Contract.Ensures(Contract.ValueAtReturn(out e0) != null); IToken/*!*/ x;  Expression/*!*/ e1; 

 		ImpliesExpliesExpression(out e0, allowSemi, allowLambda);

-		while (la.kind == 99 || la.kind == 100) {

+		while (la.kind == 100 || la.kind == 101) {

 			EquivOp();

 			x = t; 

 			ImpliesExpliesExpression(out e1, allowSemi, allowLambda);

@@ -2752,7 +2788,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 		Contract.Ensures(Contract.ValueAtReturn(out e0) != null); IToken/*!*/ x;  Expression/*!*/ e1; 

 		LogicalExpression(out e0, allowSemi, allowLambda);

 		if (StartOf(29)) {

-			if (la.kind == 101 || la.kind == 102) {

+			if (la.kind == 102 || la.kind == 103) {

 				ImpliesOp();

 				x = t; 

 				ImpliesExpression(out e1, allowSemi, allowLambda);

@@ -2762,7 +2798,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 				x = t; 

 				LogicalExpression(out e1, allowSemi, allowLambda);

 				e0 = new BinaryExpr(x, BinaryExpr.Opcode.Exp, e0, e1); 

-				while (la.kind == 103 || la.kind == 104) {

+				while (la.kind == 104 || la.kind == 105) {

 					ExpliesOp();

 					x = t; 

 					LogicalExpression(out e1, allowSemi, allowLambda);

@@ -2776,12 +2812,12 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 		Contract.Ensures(Contract.ValueAtReturn(out e0) != null); IToken/*!*/ x;  Expression/*!*/ e1; 

 		RelationalExpression(out e0, allowSemi, allowLambda);

 		if (StartOf(30)) {

-			if (la.kind == 105 || la.kind == 106) {

+			if (la.kind == 106 || la.kind == 107) {

 				AndOp();

 				x = t; 

 				RelationalExpression(out e1, allowSemi, allowLambda);

 				e0 = new BinaryExpr(x, BinaryExpr.Opcode.And, e0, e1); 

-				while (la.kind == 105 || la.kind == 106) {

+				while (la.kind == 106 || la.kind == 107) {

 					AndOp();

 					x = t; 

 					RelationalExpression(out e1, allowSemi, allowLambda);

@@ -2792,7 +2828,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 				x = t; 

 				RelationalExpression(out e1, allowSemi, allowLambda);

 				e0 = new BinaryExpr(x, BinaryExpr.Opcode.Or, e0, e1); 

-				while (la.kind == 107 || la.kind == 108) {

+				while (la.kind == 108 || la.kind == 109) {

 					OrOp();

 					x = t; 

 					RelationalExpression(out e1, allowSemi, allowLambda);

@@ -2805,7 +2841,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 	void ImpliesExpression(out Expression e0, bool allowSemi, bool allowLambda) {

 		Contract.Ensures(Contract.ValueAtReturn(out e0) != null); IToken/*!*/ x;  Expression/*!*/ e1; 

 		LogicalExpression(out e0, allowSemi, allowLambda);

-		if (la.kind == 101 || la.kind == 102) {

+		if (la.kind == 102 || la.kind == 103) {

 			ImpliesOp();

 			x = t; 

 			ImpliesExpression(out e1, allowSemi, allowLambda);

@@ -2915,25 +2951,25 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 	}

 

 	void AndOp() {

-		if (la.kind == 105) {

+		if (la.kind == 106) {

 			Get();

-		} else if (la.kind == 106) {

+		} else if (la.kind == 107) {

 			Get();

-		} else SynErr(213);

+		} else SynErr(215);

 	}

 

 	void OrOp() {

-		if (la.kind == 107) {

+		if (la.kind == 108) {

 			Get();

-		} else if (la.kind == 108) {

+		} else if (la.kind == 109) {

 			Get();

-		} else SynErr(214);

+		} else SynErr(216);

 	}

 

 	void Term(out Expression e0, bool allowSemi, bool allowLambda) {

 		Contract.Ensures(Contract.ValueAtReturn(out e0) != null); IToken/*!*/ x;  Expression/*!*/ e1;  BinaryExpr.Opcode op; 

 		Factor(out e0, allowSemi, allowLambda);

-		while (la.kind == 111 || la.kind == 112) {

+		while (la.kind == 112 || la.kind == 113) {

 			AddOp(out x, out op);

 			Factor(out e1, allowSemi, allowLambda);

 			e0 = new BinaryExpr(x, op, e0, e1); 

@@ -2947,49 +2983,49 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 		k = null;

 		

 		switch (la.kind) {

-		case 39: {

+		case 41: {

 			Get();

 			x = t;  op = BinaryExpr.Opcode.Eq; 

-			if (la.kind == 92) {

+			if (la.kind == 93) {

 				Get();

-				Expect(78);

-				Expression(out k, true, true);

 				Expect(79);

+				Expression(out k, true, true);

+				Expect(80);

 			}

 			break;

 		}

-		case 45: {

+		case 46: {

 			Get();

 			x = t;  op = BinaryExpr.Opcode.Lt; 

 			break;

 		}

-		case 46: {

+		case 47: {

 			Get();

 			x = t;  op = BinaryExpr.Opcode.Gt; 

 			break;

 		}

-		case 93: {

+		case 94: {

 			Get();

 			x = t;  op = BinaryExpr.Opcode.Le; 

 			break;

 		}

-		case 94: {

+		case 95: {

 			Get();

 			x = t;  op = BinaryExpr.Opcode.Ge; 

 			break;

 		}

-		case 95: {

+		case 96: {

 			Get();

 			x = t;  op = BinaryExpr.Opcode.Neq; 

-			if (la.kind == 92) {

+			if (la.kind == 93) {

 				Get();

-				Expect(78);

-				Expression(out k, true, true);

 				Expect(79);

+				Expression(out k, true, true);

+				Expect(80);

 			}

 			break;

 		}

-		case 109: {

+		case 110: {

 			Get();

 			x = t;  op = BinaryExpr.Opcode.In; 

 			break;

@@ -2999,10 +3035,10 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 			x = t;  op = BinaryExpr.Opcode.NotIn; 

 			break;

 		}

-		case 110: {

+		case 111: {

 			Get();

 			x = t;  y = Token.NoToken; 

-			if (la.kind == 110) {

+			if (la.kind == 111) {

 				Get();

 				y = t; 

 			}

@@ -3017,29 +3053,29 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 			

 			break;

 		}

-		case 96: {

+		case 97: {

 			Get();

 			x = t;  op = BinaryExpr.Opcode.Neq; 

 			break;

 		}

-		case 97: {

+		case 98: {

 			Get();

 			x = t;  op = BinaryExpr.Opcode.Le; 

 			break;

 		}

-		case 98: {

+		case 99: {

 			Get();

 			x = t;  op = BinaryExpr.Opcode.Ge; 

 			break;

 		}

-		default: SynErr(215); break;

+		default: SynErr(217); break;

 		}

 	}

 

 	void Factor(out Expression e0, bool allowSemi, bool allowLambda) {

 		Contract.Ensures(Contract.ValueAtReturn(out e0) != null); IToken/*!*/ x;  Expression/*!*/ e1;  BinaryExpr.Opcode op; 

 		UnaryExpression(out e0, allowSemi, allowLambda);

-		while (la.kind == 17 || la.kind == 113 || la.kind == 114) {

+		while (la.kind == 17 || la.kind == 114 || la.kind == 115) {

 			MulOp(out x, out op);

 			UnaryExpression(out e1, allowSemi, allowLambda);

 			e0 = new BinaryExpr(x, op, e0, e1); 

@@ -3048,81 +3084,81 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 

 	void AddOp(out IToken x, out BinaryExpr.Opcode op) {

 		Contract.Ensures(Contract.ValueAtReturn(out x) != null); x = Token.NoToken;  op=BinaryExpr.Opcode.Add/*(dummy)*/; 

-		if (la.kind == 111) {

+		if (la.kind == 112) {

 			Get();

 			x = t;  op = BinaryExpr.Opcode.Add; 

-		} else if (la.kind == 112) {

+		} else if (la.kind == 113) {

 			Get();

 			x = t;  op = BinaryExpr.Opcode.Sub; 

-		} else SynErr(216);

+		} else SynErr(218);

 	}

 

 	void UnaryExpression(out Expression e, bool allowSemi, bool allowLambda) {

 		Contract.Ensures(Contract.ValueAtReturn(out e) != null); IToken/*!*/ x;  e = dummyExpr; 

 		switch (la.kind) {

-		case 112: {

+		case 113: {

 			Get();

 			x = t; 

 			UnaryExpression(out e, allowSemi, allowLambda);

 			e = new NegationExpression(x, e); 

 			break;

 		}

-		case 110: case 115: {

+		case 111: case 116: {

 			NegOp();

 			x = t; 

 			UnaryExpression(out e, allowSemi, allowLambda);

 			e = new UnaryOpExpr(x, UnaryOpExpr.Opcode.Not, e); 

 			break;

 		}

-		case 31: case 36: case 61: case 71: case 77: case 80: case 85: case 86: case 88: case 91: case 124: case 125: case 126: {

+		case 31: case 36: case 62: case 72: case 77: case 81: case 86: case 87: case 89: case 92: case 125: case 126: case 127: {

 			EndlessExpression(out e, allowSemi, allowLambda);

 			break;

 		}

 		case 1: {

 			DottedIdentifiersAndFunction(out e, allowSemi, allowLambda);

-			while (la.kind == 66 || la.kind == 78) {

+			while (la.kind == 67 || la.kind == 79) {

 				Suffix(ref e);

 			}

 			ApplySuffix(ref e);

 			break;

 		}

-		case 13: case 78: {

+		case 13: case 79: {

 			DisplayExpr(out e);

-			while (la.kind == 66 || la.kind == 78) {

+			while (la.kind == 67 || la.kind == 79) {

 				Suffix(ref e);

 			}

 			break;

 		}

-		case 62: {

+		case 63: {

 			MultiSetExpr(out e);

-			while (la.kind == 66 || la.kind == 78) {

+			while (la.kind == 67 || la.kind == 79) {

 				Suffix(ref e);

 			}

 			break;

 		}

-		case 64: {

+		case 65: {

 			Get();

 			x = t; 

-			if (la.kind == 78) {

+			if (la.kind == 79) {

 				MapDisplayExpr(x, out e);

-				while (la.kind == 66 || la.kind == 78) {

+				while (la.kind == 67 || la.kind == 79) {

 					Suffix(ref e);

 				}

 			} else if (la.kind == 1) {

 				MapComprehensionExpr(x, out e, allowSemi);

 			} else if (StartOf(32)) {

 				SemErr("map must be followed by literal in brackets or comprehension."); 

-			} else SynErr(217);

+			} else SynErr(219);

 			break;

 		}

-		case 2: case 3: case 4: case 15: case 35: case 59: case 60: case 116: case 117: case 118: case 119: case 120: case 121: {

+		case 2: case 3: case 4: case 15: case 35: case 60: case 61: case 117: case 118: case 119: case 120: case 121: case 122: {

 			ConstAtomExpression(out e, allowSemi, allowLambda);

-			while (la.kind == 66 || la.kind == 78) {

+			while (la.kind == 67 || la.kind == 79) {

 				Suffix(ref e);

 			}

 			break;

 		}

-		default: SynErr(218); break;

+		default: SynErr(220); break;

 		}

 	}

 

@@ -3131,21 +3167,21 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 		if (la.kind == 17) {

 			Get();

 			x = t;  op = BinaryExpr.Opcode.Mul; 

-		} else if (la.kind == 113) {

+		} else if (la.kind == 114) {

 			Get();

 			x = t;  op = BinaryExpr.Opcode.Div; 

-		} else if (la.kind == 114) {

+		} else if (la.kind == 115) {

 			Get();

 			x = t;  op = BinaryExpr.Opcode.Mod; 

-		} else SynErr(219);

+		} else SynErr(221);

 	}

 

 	void NegOp() {

-		if (la.kind == 110) {

+		if (la.kind == 111) {

 			Get();

-		} else if (la.kind == 115) {

+		} else if (la.kind == 116) {

 			Get();

-		} else SynErr(220);

+		} else SynErr(222);

 	}

 

 	void EndlessExpression(out Expression e, bool allowSemi, bool allowLambda) {

@@ -3155,30 +3191,30 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 		e = dummyExpr;

 		

 		switch (la.kind) {

-		case 80: {

+		case 81: {

 			Get();

 			x = t; 

 			Expression(out e, true, true);

-			Expect(122);

+			Expect(123);

 			Expression(out e0, true, true);

-			Expect(81);

+			Expect(82);

 			Expression(out e1, allowSemi, allowLambda);

 			e = new ITEExpr(x, e, e0, e1); 

 			break;

 		}

-		case 85: {

+		case 86: {

 			MatchExpression(out e, allowSemi, allowLambda);

 			break;

 		}

-		case 88: case 124: case 125: case 126: {

+		case 89: case 125: case 126: case 127: {

 			QuantifierGuts(out e, allowSemi, allowLambda);

 			break;

 		}

-		case 61: {

+		case 62: {

 			ComprehensionExpr(out e, allowSemi, allowLambda);

 			break;

 		}

-		case 77: case 86: case 91: {

+		case 77: case 87: case 92: {

 			StmtInExpr(out s);

 			Expression(out e, allowSemi, allowLambda);

 			e = new StmtExpr(s.Tok, s, e); 

@@ -3188,11 +3224,11 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 			LetExpr(out e, allowSemi, allowLambda);

 			break;

 		}

-		case 71: {

+		case 72: {

 			NamedExpr(out e, allowSemi, allowLambda);

 			break;

 		}

-		default: SynErr(221); break;

+		default: SynErr(223); break;

 		}

 	}

 

@@ -3205,20 +3241,20 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 		

 		Ident(out id);

 		idents.Add(id); 

-		while (la.kind == 66) {

+		while (la.kind == 67) {

 			IdentOrDigitsSuffix(out id, out idPrime);

 			idents.Add(id);

 			if (idPrime != null) { idents.Add(idPrime); id = idPrime; }

 			

 		}

-		if (la.kind == 15 || la.kind == 92) {

+		if (la.kind == 15 || la.kind == 93) {

 			args = new List<Expression>(); 

-			if (la.kind == 92) {

+			if (la.kind == 93) {

 				Get();

 				id.val = id.val + "#";  Expression k; 

-				Expect(78);

-				Expression(out k, true, true);

 				Expect(79);

+				Expression(out k, true, true);

+				Expect(80);

 				args.Add(k); 

 			}

 			Expect(15);

@@ -3262,7 +3298,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 		List<Expression> multipleIndices = null;

 		bool func = false;

 		

-		if (la.kind == 66) {

+		if (la.kind == 67) {

 			IdentOrDigitsSuffix(out id, out x);

 			if (x != null) {

 			 // process id as a Suffix in its own right

@@ -3270,14 +3306,14 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 			 id = x;  // move to the next Suffix

 			}

 			

-			if (la.kind == 15 || la.kind == 92) {

+			if (la.kind == 15 || la.kind == 93) {

 				args = new List<Expression/*!*/>();  func = true; 

-				if (la.kind == 92) {

+				if (la.kind == 93) {

 					Get();

 					id.val = id.val + "#";  Expression k; 

-					Expect(78);

-					Expression(out k, true, true);

 					Expect(79);

+					Expression(out k, true, true);

+					Expect(80);

 					args.Add(k); 

 				}

 				Expect(15);

@@ -3289,13 +3325,13 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 				e = new FunctionCallExpr(id, id.val, e, openParen, args); 

 			}

 			if (!func) { e = new ExprDotName(id, e, id.val); } 

-		} else if (la.kind == 78) {

+		} else if (la.kind == 79) {

 			Get();

 			x = t; 

 			if (StartOf(17)) {

 				Expression(out ee, true, true);

 				e0 = ee; 

-				if (la.kind == 123) {

+				if (la.kind == 124) {

 					Get();

 					anyDots = true; 

 					if (StartOf(17)) {

@@ -3306,7 +3342,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 					Get();

 					Expression(out ee, true, true);

 					e1 = ee; 

-				} else if (la.kind == 7 || la.kind == 79) {

+				} else if (la.kind == 7 || la.kind == 80) {

 					while (la.kind == 7) {

 						Get();

 						if (multipleLengths == null) {

@@ -3322,7 +3358,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 							

 						}

 					}

-				} else if (la.kind == 37 || la.kind == 79) {

+				} else if (la.kind == 37 || la.kind == 80) {

 					while (la.kind == 37) {

 						Get();

 						Expression(out ee, true, true);

@@ -3333,15 +3369,15 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 						multipleIndices.Add(ee);

 						

 					}

-				} else SynErr(222);

-			} else if (la.kind == 123) {

+				} else SynErr(224);

+			} else if (la.kind == 124) {

 				Get();

 				anyDots = true; 

 				if (StartOf(17)) {

 					Expression(out ee, true, true);

 					e1 = ee; 

 				}

-			} else SynErr(223);

+			} else SynErr(225);

 			if (multipleIndices != null) {

 			 e = new MultiSelectExpr(x, e, multipleIndices);

 			 // make sure an array class with this dimensionality exists

@@ -3381,8 +3417,8 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 			 }

 			}

 			

-			Expect(79);

-		} else SynErr(224);

+			Expect(80);

+		} else SynErr(226);

 		ApplySuffix(ref e);

 	}

 

@@ -3411,15 +3447,15 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 			}

 			e = new SetDisplayExpr(x, elements);

 			Expect(14);

-		} else if (la.kind == 78) {

+		} else if (la.kind == 79) {

 			Get();

 			x = t;  elements = new List<Expression/*!*/>(); 

 			if (StartOf(17)) {

 				Expressions(elements);

 			}

 			e = new SeqDisplayExpr(x, elements); 

-			Expect(79);

-		} else SynErr(225);

+			Expect(80);

+		} else SynErr(227);

 	}

 

 	void MultiSetExpr(out Expression e) {

@@ -3427,7 +3463,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 		IToken/*!*/ x = null;  List<Expression/*!*/>/*!*/ elements;

 		e = dummyExpr;

 		

-		Expect(62);

+		Expect(63);

 		x = t; 

 		if (la.kind == 13) {

 			Get();

@@ -3445,7 +3481,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 			Expect(16);

 		} else if (StartOf(32)) {

 			SemErr("multiset must be followed by multiset literal or expression to coerce in parentheses."); 

-		} else SynErr(226);

+		} else SynErr(228);

 	}

 

 	void MapDisplayExpr(IToken/*!*/ mapToken, out Expression e) {

@@ -3453,12 +3489,12 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 		List<ExpressionPair/*!*/>/*!*/ elements= new List<ExpressionPair/*!*/>() ;

 		e = dummyExpr;

 		

-		Expect(78);

+		Expect(79);

 		if (StartOf(17)) {

 			MapLiteralExpressions(out elements);

 		}

 		e = new MapDisplayExpr(mapToken, elements);

-		Expect(79);

+		Expect(80);

 	}

 

 	void MapComprehensionExpr(IToken mapToken, out Expression e, bool allowSemi) {

@@ -3486,17 +3522,17 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 		e = dummyExpr;  Type toType = null;

 		

 		switch (la.kind) {

-		case 116: {

+		case 117: {

 			Get();

 			e = new LiteralExpr(t, false); 

 			break;

 		}

-		case 117: {

+		case 118: {

 			Get();

 			e = new LiteralExpr(t, true); 

 			break;

 		}

-		case 118: {

+		case 119: {

 			Get();

 			e = new LiteralExpr(t); 

 			break;

@@ -3511,12 +3547,12 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 			e = new LiteralExpr(t, d); 

 			break;

 		}

-		case 119: {

+		case 120: {

 			Get();

 			e = new ThisExpr(t); 

 			break;

 		}

-		case 120: {

+		case 121: {

 			Get();

 			x = t; 

 			Expect(15);

@@ -3525,7 +3561,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 			e = new UnaryOpExpr(x, UnaryOpExpr.Opcode.Fresh, e); 

 			break;

 		}

-		case 121: {

+		case 122: {

 			Get();

 			x = t; 

 			Expect(15);

@@ -3542,8 +3578,8 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 			Expect(35);

 			break;

 		}

-		case 59: case 60: {

-			if (la.kind == 59) {

+		case 60: case 61: {

+			if (la.kind == 60) {

 				Get();

 				x = t; toType = new IntType(); 

 			} else {

@@ -3560,7 +3596,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 			ParensExpression(out e, allowSemi, allowLambda);

 			break;

 		}

-		default: SynErr(227); break;

+		default: SynErr(229); break;

 		}

 	}

 

@@ -3585,7 +3621,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 			 n = BigInteger.Zero;

 			}

 			

-		} else SynErr(228);

+		} else SynErr(230);

 	}

 

 	void Dec(out Basetypes.BigDec d) {

@@ -3693,7 +3729,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 		} else if (la.kind == 10) {

 			Get();

 			oneShot = true; 

-		} else SynErr(229);

+		} else SynErr(231);

 	}

 

 	void OptTypedExpr(out Expression e, out Type tt, bool allowSemi) {

@@ -3722,11 +3758,11 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 	}

 

 	void QSep() {

-		if (la.kind == 127) {

+		if (la.kind == 128) {

 			Get();

-		} else if (la.kind == 128) {

+		} else if (la.kind == 129) {

 			Get();

-		} else SynErr(230);

+		} else SynErr(232);

 	}

 

 	void MatchExpression(out Expression e, bool allowSemi, bool allowLambda) {

@@ -3734,14 +3770,14 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 		List<MatchCaseExpr/*!*/> cases = new List<MatchCaseExpr/*!*/>();

 		bool usesOptionalBrace = false;

 		

-		Expect(85);

+		Expect(86);

 		x = t; 

 		Expression(out e, allowSemi, true);

 		if (la.kind == 13) {

 			Get();

 			usesOptionalBrace = true; 

 		}

-		while (la.kind == 82) {

+		while (la.kind == 83) {

 			CaseExpression(out c, allowSemi, usesOptionalBrace || allowLambda);

 			cases.Add(c); 

 		}

@@ -3749,7 +3785,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 			Expect(14);

 		} else if (StartOf(32)) {

 			if (usesOptionalBrace) { SemErr(t, "expecting close curly brace"); } 

-		} else SynErr(231);

+		} else SynErr(233);

 		e = new MatchExpr(x, e, cases, usesOptionalBrace); 

 	}

 

@@ -3761,13 +3797,13 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 		Expression range;

 		Expression/*!*/ body;

 		

-		if (la.kind == 88 || la.kind == 124) {

+		if (la.kind == 89 || la.kind == 125) {

 			Forall();

 			x = t;  univ = true; 

-		} else if (la.kind == 125 || la.kind == 126) {

+		} else if (la.kind == 126 || la.kind == 127) {

 			Exists();

 			x = t; 

-		} else SynErr(232);

+		} else SynErr(234);

 		QuantifierDomain(out bvars, out attrs, out range);

 		QSep();

 		Expression(out body, allowSemi, allowLambda);

@@ -3787,7 +3823,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 		Expression range;

 		Expression body = null;

 		

-		Expect(61);

+		Expect(62);

 		x = t; 

 		IdentTypeOptional(out bv);

 		bvars.Add(bv); 

@@ -3798,7 +3834,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 		}

 		Expect(35);

 		Expression(out range, allowSemi, allowLambda);

-		if (la.kind == 127 || la.kind == 128) {

+		if (la.kind == 128 || la.kind == 129) {

 			QSep();

 			Expression(out body, allowSemi, allowLambda);

 		}

@@ -3809,13 +3845,13 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 

 	void StmtInExpr(out Statement s) {

 		s = dummyStmt; 

-		if (la.kind == 86) {

+		if (la.kind == 87) {

 			AssertStmt(out s);

 		} else if (la.kind == 77) {

 			AssumeStmt(out s);

-		} else if (la.kind == 91) {

+		} else if (la.kind == 92) {

 			CalcStmt(out s);

-		} else SynErr(233);

+		} else SynErr(235);

 	}

 

 	void LetExpr(out Expression e, bool allowSemi, bool allowLambda) {

@@ -3855,7 +3891,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 			 }

 			}

 			

-		} else SynErr(234);

+		} else SynErr(236);

 		Expression(out e, false, true);

 		letRHSs.Add(e); 

 		while (la.kind == 37) {

@@ -3873,7 +3909,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 		e = dummyExpr;

 		Expression expr;

 		

-		Expect(71);

+		Expect(72);

 		x = t; 

 		NoUSIdent(out d);

 		Expect(7);

@@ -3906,7 +3942,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 			IdentTypeOptional(out bv);

 			pat = new CasePattern(bv.tok, bv);

 			

-		} else SynErr(235);

+		} else SynErr(237);

 	}

 

 	void CaseExpression(out MatchCaseExpr c, bool allowSemi, bool allowLambda) {

@@ -3915,7 +3951,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 		BoundVar/*!*/ bv;

 		Expression/*!*/ body;

 		

-		Expect(82);

+		Expect(83);

 		x = t; 

 		Ident(out id);

 		if (la.kind == 15) {

@@ -3935,19 +3971,19 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 	}

 

 	void Forall() {

-		if (la.kind == 88) {

+		if (la.kind == 89) {

 			Get();

-		} else if (la.kind == 124) {

+		} else if (la.kind == 125) {

 			Get();

-		} else SynErr(236);

+		} else SynErr(238);

 	}

 

 	void Exists() {

-		if (la.kind == 125) {

+		if (la.kind == 126) {

 			Get();

-		} else if (la.kind == 126) {

+		} else if (la.kind == 127) {

 			Get();

-		} else SynErr(237);

+		} else SynErr(239);

 	}

 

 	void AttributeBody(ref Attributes attrs) {

@@ -3983,40 +4019,40 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 	}

 

 	static readonly bool[,]/*!*/ set = {

-		{T,T,T,T, T,x,x,x, T,x,x,T, T,T,x,T, x,x,x,x, x,x,x,x, x,x,x,x, T,x,T,T, x,T,T,T, T,x,x,x, x,T,x,x, T,x,x,T, T,T,T,T, T,T,T,T, T,x,x,T, T,x,x,x, x,x,x,x, x,x,x,T, T,x,x,T, x,T,x,x, T,x,x,T, T,T,T,T, T,T,T,T, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, T,T,T,T, T,T,x,x, x,x,x,x, x,x,x},

-		{x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, T,T,x,T, x,x,x,x, T,x,T,T, T,T,T,x, T,x,T,x, x,T,x,x, x,x,x,T, T,T,T,T, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,T, T,T,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x},

-		{x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,T, T,x,x,x, T,x,x,x, x,x,x,x, x,x,x,T, T,T,T,T, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,T, T,T,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x},

-		{T,x,x,x, x,x,x,x, T,x,x,x, x,x,T,x, x,x,x,x, T,T,x,T, x,T,x,x, T,x,T,T, T,T,T,x, T,x,T,x, x,T,x,x, x,T,x,T, T,T,T,T, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,T, T,T,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x},

-		{x,T,x,x, x,T,x,x, x,x,x,x, x,x,x,T, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,T,T,T, T,T,T,T, T,T,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x},

-		{x,x,x,x, x,x,x,x, x,x,x,T, T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, T,T,T,T, T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x},

-		{x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,T, T,T,T,T, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x},

-		{T,x,x,x, x,x,x,x, x,x,x,T, T,T,T,T, x,x,x,x, T,T,x,T, x,x,x,x, T,x,T,T, T,T,T,x, T,x,T,x, x,T,x,x, x,T,x,T, T,T,T,T, x,x,T,T, x,x,x,x, x,x,x,x, x,x,x,T, T,T,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x},

-		{x,x,x,x, x,x,x,x, x,x,x,T, T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,T,T, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x},

-		{T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,T, T,T,T,T, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x},

-		{x,x,x,x, x,x,x,x, x,x,x,x, T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, T,T,T,T, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x},

-		{x,T,T,x, x,T,x,x, x,x,x,x, x,x,x,T, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,T, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,T,T,T, T,T,T,T, T,T,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x},

-		{T,x,x,x, x,x,x,x, x,x,x,T, T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, T,T,T,T, T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x},

-		{x,T,T,T, T,x,x,x, x,x,x,x, x,T,x,T, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,T, x,x,x,T, T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,T, T,T,T,x, T,x,x,x, x,x,T,T, x,x,x,x, x,T,T,x, T,x,x,x, x,T,T,x, T,x,x,T, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,T,x, T,x,x,T, T,T,T,T, T,T,x,x, T,T,T,x, x,x,x},

-		{x,x,x,x, x,x,x,x, x,x,x,x, T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,T,T,x, T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x},

-		{x,T,T,T, T,x,x,x, x,x,x,x, x,T,x,T, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,T, x,x,x,T, T,x,x,x, x,x,x,x, T,x,x,x, x,x,x,x, x,x,x,x, T,x,x,T, T,x,x,x, x,x,x,x, x,x,x,T, T,x,x,T, x,T,x,x, T,x,x,T, x,T,T,T, T,T,T,T, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, T,T,T,T, T,T,x,x, x,x,x,x, x,x,x},

-		{T,x,x,x, x,x,x,x, x,x,x,x, T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, T,T,T,T, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x},

-		{x,T,T,T, T,x,x,x, x,x,x,x, x,T,x,T, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,T, x,x,x,T, T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,T, T,T,T,x, T,x,x,x, x,x,x,T, x,x,x,x, x,T,T,x, T,x,x,x, x,T,T,x, T,x,x,T, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,T,x, T,x,x,T, T,T,T,T, T,T,x,x, T,T,T,x, x,x,x},

-		{x,T,T,T, T,x,x,x, x,x,x,x, x,T,x,T, x,T,x,x, x,x,x,x, x,x,x,x, x,x,x,T, x,x,x,T, T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,T, T,T,T,x, T,x,x,x, x,x,T,T, x,x,x,x, x,T,T,x, T,x,x,x, x,T,T,x, T,x,x,T, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,T,x, T,x,x,T, T,T,T,T, T,T,x,x, T,T,T,x, x,x,x},

-		{T,T,T,T, T,x,x,x, x,x,x,x, x,T,x,T, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,T, x,x,x,T, T,x,x,x, x,x,x,x, T,x,x,x, x,x,x,x, x,x,x,x, T,x,x,T, T,x,x,x, x,x,x,x, x,x,x,T, T,x,x,T, x,T,x,x, T,x,x,T, x,T,T,T, T,T,T,T, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, T,T,T,T, T,T,x,x, x,x,x,x, x,x,x},

-		{x,T,T,T, T,x,x,x, x,x,x,x, x,T,x,T, x,T,x,x, x,x,x,x, x,x,x,x, x,x,x,T, x,x,x,T, T,x,x,x, x,x,x,x, T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,T, T,T,T,x, T,x,x,x, x,x,x,T, x,x,x,x, x,T,T,x, T,x,x,x, x,T,T,x, T,x,x,T, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,T,x, T,x,x,T, T,T,T,T, T,T,x,x, T,T,T,x, x,x,x},

-		{x,T,T,T, T,x,x,x, x,x,x,x, x,T,x,T, x,T,x,x, x,x,x,x, x,x,x,x, x,x,x,T, x,x,x,T, T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,T, T,T,T,x, T,x,x,x, x,x,x,T, x,x,x,x, x,T,T,x, T,x,x,x, x,T,T,x, T,x,x,T, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,T,x, T,x,x,T, T,T,T,T, T,T,x,x, T,T,T,x, x,x,x},

-		{x,T,T,T, T,x,x,x, x,x,x,x, x,T,T,T, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,T, x,x,x,T, T,x,x,x, x,x,x,x, T,x,x,x, x,x,x,x, x,x,x,x, T,x,x,T, T,x,x,x, x,x,x,x, x,x,x,T, T,x,x,T, x,T,x,x, T,x,T,T, x,T,T,T, T,T,T,T, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, T,T,T,T, T,T,x,x, x,x,x,x, x,x,x},

-		{x,T,T,T, T,x,x,x, x,x,x,x, x,T,T,T, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,T, x,x,x,T, T,x,x,x, x,x,x,x, T,x,x,x, x,x,x,x, x,T,T,x, T,x,x,T, T,x,x,x, x,x,x,x, x,x,x,T, T,x,x,T, x,T,x,x, T,x,T,T, x,T,T,T, T,T,T,T, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, T,T,T,T, T,T,x,x, x,x,x,x, x,x,x},

-		{x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,T, x,x,x,x, x,T,T,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,T,T,T, T,T,T,T, T,T,T,T, T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x},

-		{x,T,T,T, T,x,x,x, x,x,x,x, x,T,x,T, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,T, x,x,x,T, T,x,x,x, x,x,x,x, T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,T, T,T,T,x, T,x,x,x, x,x,T,T, x,x,x,x, x,T,T,x, T,x,x,x, x,T,T,x, T,x,x,T, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,T,x, T,x,x,T, T,T,T,T, T,T,x,x, T,T,T,x, x,x,x},

-		{x,T,T,T, T,x,x,x, x,x,x,x, x,T,x,T, x,T,x,x, x,x,x,x, x,x,x,x, x,x,x,T, x,x,x,T, T,x,x,x, T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,T, T,T,T,x, T,x,x,x, x,x,x,T, x,x,x,x, x,T,T,x, T,x,x,x, x,T,T,x, T,x,x,T, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,T,x, T,x,x,T, T,T,T,T, T,T,x,x, T,T,T,x, x,x,x},

-		{x,x,T,T, T,x,x,x, x,x,x,x, x,x,x,T, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,T, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,T, T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, T,T,T,T, T,T,x,x, x,x,x,x, x,x,x},

-		{x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, T,T,x,T, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x},

-		{x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,T,T,T, T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x},

-		{x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,T,T,T, T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x},

-		{x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,T,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,T, x,x,x,x, x,T,T,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,T,T,T, T,T,T,x, x,x,x,x, x,x,x,x, x,T,T,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x},

-		{x,T,T,T, T,x,x,T, T,T,T,T, T,T,T,T, T,T,T,x, x,x,x,x, x,x,x,x, x,x,x,T, x,x,x,T, T,T,x,T, x,x,x,x, T,T,T,x, x,x,x,x, T,T,T,T, T,x,x,T, T,x,x,x, x,x,T,x, x,x,T,T, T,x,T,T, T,T,T,T, T,T,T,T, T,T,T,T, T,T,T,T, x,T,T,T, T,T,T,T, T,T,T,T, T,T,T,T, T,T,T,T, T,T,T,x, T,T,T,T, T,T,T,T, x,x,x,T, T,x,x},

-		{x,T,T,T, T,x,T,x, x,x,x,x, x,T,x,T, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,T, x,x,x,T, T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,T, T,T,T,x, T,x,x,x, x,x,x,T, x,x,x,x, x,T,T,x, T,x,x,x, x,T,T,x, T,x,x,T, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,T,x, T,x,x,T, T,T,T,T, T,T,x,x, T,T,T,x, x,x,x}

+		{T,T,T,T, T,x,x,x, T,x,x,T, T,T,x,T, x,x,x,x, x,x,x,x, x,x,x,x, T,x,T,T, x,T,T,T, T,x,x,x, x,x,T,x, x,T,x,x, T,T,T,T, T,T,T,T, T,T,x,x, T,T,x,x, x,x,x,x, x,x,x,x, T,T,x,T, x,T,x,x, x,T,x,x, T,T,T,T, T,T,T,T, T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,T,T,T, T,T,T,x, x,x,x,x, x,x,x,x},

+		{x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, T,T,x,T, x,x,x,x, T,x,T,T, T,T,T,x, T,x,T,x, T,x,T,x, x,x,x,x, T,T,T,T, T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, T,T,T,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x},

+		{x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,T, T,x,x,x, T,x,x,x, x,x,x,x, x,x,x,x, T,T,T,T, T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, T,T,T,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x},

+		{x,T,x,x, x,T,x,x, x,x,x,x, x,x,x,T, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,T,T, T,T,T,T, T,T,T,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x},

+		{T,x,x,x, x,x,x,x, T,x,x,x, x,x,T,x, x,x,x,x, T,T,x,T, x,T,x,x, T,x,T,T, T,T,T,x, T,x,T,x, T,x,T,x, x,x,T,x, T,T,T,T, T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, T,T,T,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x},

+		{x,x,x,x, x,x,x,x, x,x,x,T, T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,T,T,T, T,T,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x},

+		{x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, T,T,T,T, T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x},

+		{T,x,x,x, x,x,x,x, x,x,x,T, T,T,T,T, x,x,x,x, T,T,x,T, x,x,x,x, T,x,T,T, T,T,T,x, T,x,T,x, T,x,T,x, x,x,T,x, T,T,T,T, T,x,x,T, T,x,x,x, x,x,x,x, x,x,x,x, T,T,T,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x},

+		{x,x,x,x, x,x,x,x, x,x,x,T, T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,T, T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x},

+		{T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, T,T,T,T, T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x},

+		{x,x,x,x, x,x,x,x, x,x,x,x, T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,T,T,T, T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x},

+		{x,T,T,x, x,T,x,x, x,x,x,x, x,x,x,T, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,T, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,T,T, T,T,T,T, T,T,T,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x},

+		{T,x,x,x, x,x,x,x, x,x,x,T, T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,T,T,T, T,T,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x},

+		{x,T,T,T, T,x,x,x, x,x,x,x, x,T,x,T, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,T, x,x,x,T, T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, T,T,T,T, x,T,x,x, x,x,x,T, T,x,x,x, x,T,x,T, x,T,x,x, x,x,T,T, x,T,x,x, T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,T, x,T,x,x, T,T,T,T, T,T,T,x, x,T,T,T, x,x,x,x},

+		{x,x,x,x, x,x,x,x, x,x,x,x, T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,T,T, x,T,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x},

+		{x,T,T,T, T,x,x,x, x,x,x,x, x,T,x,T, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,T, x,x,x,T, T,x,x,x, x,x,x,x, x,T,x,x, x,x,x,x, x,x,x,x, x,T,x,x, T,T,x,x, x,x,x,x, x,x,x,x, T,T,x,T, x,T,x,x, x,T,x,x, T,x,T,T, T,T,T,T, T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,T,T,T, T,T,T,x, x,x,x,x, x,x,x,x},

+		{T,x,x,x, x,x,x,x, x,x,x,x, T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,T,T,T, T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x},

+		{x,T,T,T, T,x,x,x, x,x,x,x, x,T,x,T, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,T, x,x,x,T, T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, T,T,T,T, x,T,x,x, x,x,x,x, T,x,x,x, x,T,x,T, x,T,x,x, x,x,T,T, x,T,x,x, T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,T, x,T,x,x, T,T,T,T, T,T,T,x, x,T,T,T, x,x,x,x},

+		{x,T,T,T, T,x,x,x, x,x,x,x, x,T,x,T, x,T,x,x, x,x,x,x, x,x,x,x, x,x,x,T, x,x,x,T, T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, T,T,T,T, x,T,x,x, x,x,x,T, T,x,x,x, x,T,x,T, x,T,x,x, x,x,T,T, x,T,x,x, T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,T, x,T,x,x, T,T,T,T, T,T,T,x, x,T,T,T, x,x,x,x},

+		{T,T,T,T, T,x,x,x, x,x,x,x, x,T,x,T, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,T, x,x,x,T, T,x,x,x, x,x,x,x, x,T,x,x, x,x,x,x, x,x,x,x, x,T,x,x, T,T,x,x, x,x,x,x, x,x,x,x, T,T,x,T, x,T,x,x, x,T,x,x, T,x,T,T, T,T,T,T, T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,T,T,T, T,T,T,x, x,x,x,x, x,x,x,x},

+		{x,T,T,T, T,x,x,x, x,x,x,x, x,T,x,T, x,T,x,x, x,x,x,x, x,x,x,x, x,x,x,T, x,x,x,T, T,x,x,x, x,x,x,x, x,T,x,x, x,x,x,x, x,x,x,x, x,x,x,x, T,T,T,T, x,T,x,x, x,x,x,x, T,x,x,x, x,T,x,T, x,T,x,x, x,x,T,T, x,T,x,x, T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,T, x,T,x,x, T,T,T,T, T,T,T,x, x,T,T,T, x,x,x,x},

+		{x,T,T,T, T,x,x,x, x,x,x,x, x,T,x,T, x,T,x,x, x,x,x,x, x,x,x,x, x,x,x,T, x,x,x,T, T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, T,T,T,T, x,T,x,x, x,x,x,x, T,x,x,x, x,T,x,T, x,T,x,x, x,x,T,T, x,T,x,x, T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,T, x,T,x,x, T,T,T,T, T,T,T,x, x,T,T,T, x,x,x,x},

+		{x,T,T,T, T,x,x,x, x,x,x,x, x,T,T,T, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,T, x,x,x,T, T,x,x,x, x,x,x,x, x,T,x,x, x,x,x,x, x,x,x,x, x,T,x,x, T,T,x,x, x,x,x,x, x,x,x,x, T,T,x,T, x,T,x,x, x,T,x,T, T,x,T,T, T,T,T,T, T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,T,T,T, T,T,T,x, x,x,x,x, x,x,x,x},

+		{x,T,T,T, T,x,x,x, x,x,x,x, x,T,T,T, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,T, x,x,x,T, T,x,x,x, x,x,x,x, x,T,x,x, x,x,x,x, x,x,T,T, x,T,x,x, T,T,x,x, x,x,x,x, x,x,x,x, T,T,x,T, x,T,x,x, x,T,x,T, T,x,T,T, T,T,T,T, T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,T,T,T, T,T,T,x, x,x,x,x, x,x,x,x},

+		{x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,T,x,x, x,x,T,T, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,T,T, T,T,T,T, T,T,T,T, T,T,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x},

+		{x,T,T,T, T,x,x,x, x,x,x,x, x,T,x,T, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,T, x,x,x,T, T,x,x,x, x,x,x,x, x,T,x,x, x,x,x,x, x,x,x,x, x,x,x,x, T,T,T,T, x,T,x,x, x,x,x,T, T,x,x,x, x,T,x,T, x,T,x,x, x,x,T,T, x,T,x,x, T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,T, x,T,x,x, T,T,T,T, T,T,T,x, x,T,T,T, x,x,x,x},

+		{x,T,T,T, T,x,x,x, x,x,x,x, x,T,x,T, x,T,x,x, x,x,x,x, x,x,x,x, x,x,x,T, x,x,x,T, T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, T,T,T,T, x,T,x,x, x,x,x,x, T,x,x,x, x,T,T,T, x,T,x,x, x,x,T,T, x,T,x,x, T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,T, x,T,x,x, T,T,T,T, T,T,T,x, x,T,T,T, x,x,x,x},

+		{x,x,T,T, T,x,x,x, x,x,x,x, x,x,x,T, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,T, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, T,T,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,T,T,T, T,T,T,x, x,x,x,x, x,x,x,x},

+		{x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,T,T,x, T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,T,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x},

+		{x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,T,T, T,T,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x},

+		{x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,T,T, T,T,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x},

+		{x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,T,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,T,x,x, x,x,T,T, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,T,T, T,T,T,T, x,x,x,x, x,x,x,x, x,x,T,T, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x},

+		{T,T,T,T, T,x,x,T, T,T,T,T, T,T,T,T, T,T,T,x, T,T,x,T, x,x,x,x, T,x,T,T, T,T,T,T, T,T,T,x, T,T,T,x, x,T,T,T, T,T,T,T, T,T,T,T, T,T,x,x, T,T,x,x, x,x,x,T, T,T,T,T, T,T,T,T, T,T,x,T, T,T,T,T, T,T,T,T, T,T,T,T, T,x,T,T, T,T,T,T, T,T,T,T, T,T,T,T, T,T,T,T, T,T,T,T, x,T,T,T, T,T,T,T, T,x,x,x, T,T,x,x},

+		{x,T,T,T, T,x,T,x, x,x,x,x, x,T,x,T, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,T, x,x,x,T, T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, T,T,T,T, x,T,x,x, x,x,x,x, T,x,x,x, x,T,x,T, x,T,x,x, x,x,T,T, x,T,x,x, T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,T, x,T,x,x, T,T,T,T, T,T,T,x, x,T,T,T, x,x,x,x}

 

 	};

 } // end Parser

@@ -4079,206 +4115,208 @@ public class Errors {
 			case 35: s = "\"|\" expected"; break;

 			case 36: s = "\"var\" expected"; break;

 			case 37: s = "\",\" expected"; break;

-			case 38: s = "\"type\" expected"; break;

-			case 39: s = "\"==\" expected"; break;

-			case 40: s = "\"new\" expected"; break;

-			case 41: s = "\"iterator\" expected"; break;

-			case 42: s = "\"yields\" expected"; break;

-			case 43: s = "\"returns\" expected"; break;

-			case 44: s = "\"...\" expected"; break;

-			case 45: s = "\"<\" expected"; break;

-			case 46: s = "\">\" expected"; break;

-			case 47: s = "\"method\" expected"; break;

-			case 48: s = "\"lemma\" expected"; break;

-			case 49: s = "\"colemma\" expected"; break;

-			case 50: s = "\"comethod\" expected"; break;

-			case 51: s = "\"constructor\" expected"; break;

-			case 52: s = "\"modifies\" expected"; break;

-			case 53: s = "\"free\" expected"; break;

-			case 54: s = "\"ensures\" expected"; break;

-			case 55: s = "\"decreases\" expected"; break;

-			case 56: s = "\"yield\" expected"; break;

-			case 57: s = "\"bool\" expected"; break;

-			case 58: s = "\"nat\" expected"; break;

-			case 59: s = "\"int\" expected"; break;

-			case 60: s = "\"real\" expected"; break;

-			case 61: s = "\"set\" expected"; break;

-			case 62: s = "\"multiset\" expected"; break;

-			case 63: s = "\"seq\" expected"; break;

-			case 64: s = "\"map\" expected"; break;

-			case 65: s = "\"object\" expected"; break;

-			case 66: s = "\".\" expected"; break;

-			case 67: s = "\"function\" expected"; break;

-			case 68: s = "\"predicate\" expected"; break;

-			case 69: s = "\"copredicate\" expected"; break;

-			case 70: s = "\"`\" expected"; break;

-			case 71: s = "\"label\" expected"; break;

-			case 72: s = "\"break\" expected"; break;

-			case 73: s = "\"where\" expected"; break;

+			case 38: s = "\"newtype\" expected"; break;

+			case 39: s = "\"where\" expected"; break;

+			case 40: s = "\"type\" expected"; break;

+			case 41: s = "\"==\" expected"; break;

+			case 42: s = "\"iterator\" expected"; break;

+			case 43: s = "\"yields\" expected"; break;

+			case 44: s = "\"returns\" expected"; break;

+			case 45: s = "\"...\" expected"; break;

+			case 46: s = "\"<\" expected"; break;

+			case 47: s = "\">\" expected"; break;

+			case 48: s = "\"method\" expected"; break;

+			case 49: s = "\"lemma\" expected"; break;

+			case 50: s = "\"colemma\" expected"; break;

+			case 51: s = "\"comethod\" expected"; break;

+			case 52: s = "\"constructor\" expected"; break;

+			case 53: s = "\"modifies\" expected"; break;

+			case 54: s = "\"free\" expected"; break;

+			case 55: s = "\"ensures\" expected"; break;

+			case 56: s = "\"decreases\" expected"; break;

+			case 57: s = "\"yield\" expected"; break;

+			case 58: s = "\"bool\" expected"; break;

+			case 59: s = "\"nat\" expected"; break;

+			case 60: s = "\"int\" expected"; break;

+			case 61: s = "\"real\" expected"; break;

+			case 62: s = "\"set\" expected"; break;

+			case 63: s = "\"multiset\" expected"; break;

+			case 64: s = "\"seq\" expected"; break;

+			case 65: s = "\"map\" expected"; break;

+			case 66: s = "\"object\" expected"; break;

+			case 67: s = "\".\" expected"; break;

+			case 68: s = "\"function\" expected"; break;

+			case 69: s = "\"predicate\" expected"; break;

+			case 70: s = "\"copredicate\" expected"; break;

+			case 71: s = "\"`\" expected"; break;

+			case 72: s = "\"label\" expected"; break;

+			case 73: s = "\"break\" expected"; break;

 			case 74: s = "\":=\" expected"; break;

 			case 75: s = "\"return\" expected"; break;

 			case 76: s = "\":|\" expected"; break;

 			case 77: s = "\"assume\" expected"; break;

-			case 78: s = "\"[\" expected"; break;

-			case 79: s = "\"]\" expected"; break;

-			case 80: s = "\"if\" expected"; break;

-			case 81: s = "\"else\" expected"; break;

-			case 82: s = "\"case\" expected"; break;

-			case 83: s = "\"while\" expected"; break;

-			case 84: s = "\"invariant\" expected"; break;

-			case 85: s = "\"match\" expected"; break;

-			case 86: s = "\"assert\" expected"; break;

-			case 87: s = "\"print\" expected"; break;

-			case 88: s = "\"forall\" expected"; break;

-			case 89: s = "\"parallel\" expected"; break;

-			case 90: s = "\"modify\" expected"; break;

-			case 91: s = "\"calc\" expected"; break;

-			case 92: s = "\"#\" expected"; break;

-			case 93: s = "\"<=\" expected"; break;

-			case 94: s = "\">=\" expected"; break;

-			case 95: s = "\"!=\" expected"; break;

-			case 96: s = "\"\\u2260\" expected"; break;

-			case 97: s = "\"\\u2264\" expected"; break;

-			case 98: s = "\"\\u2265\" expected"; break;

-			case 99: s = "\"<==>\" expected"; break;

-			case 100: s = "\"\\u21d4\" expected"; break;

-			case 101: s = "\"==>\" expected"; break;

-			case 102: s = "\"\\u21d2\" expected"; break;

-			case 103: s = "\"<==\" expected"; break;

-			case 104: s = "\"\\u21d0\" expected"; break;

-			case 105: s = "\"&&\" expected"; break;

-			case 106: s = "\"\\u2227\" expected"; break;

-			case 107: s = "\"||\" expected"; break;

-			case 108: s = "\"\\u2228\" expected"; break;

-			case 109: s = "\"in\" expected"; break;

-			case 110: s = "\"!\" expected"; break;

-			case 111: s = "\"+\" expected"; break;

-			case 112: s = "\"-\" expected"; break;

-			case 113: s = "\"/\" expected"; break;

-			case 114: s = "\"%\" expected"; break;

-			case 115: s = "\"\\u00ac\" expected"; break;

-			case 116: s = "\"false\" expected"; break;

-			case 117: s = "\"true\" expected"; break;

-			case 118: s = "\"null\" expected"; break;

-			case 119: s = "\"this\" expected"; break;

-			case 120: s = "\"fresh\" expected"; break;

-			case 121: s = "\"old\" expected"; break;

-			case 122: s = "\"then\" expected"; break;

-			case 123: s = "\"..\" expected"; break;

-			case 124: s = "\"\\u2200\" expected"; break;

-			case 125: s = "\"exists\" expected"; break;

-			case 126: s = "\"\\u2203\" expected"; break;

-			case 127: s = "\"::\" expected"; break;

-			case 128: s = "\"\\u2022\" expected"; break;

-			case 129: s = "??? expected"; break;

-			case 130: s = "this symbol not expected in SubModuleDecl"; break;

-			case 131: s = "invalid SubModuleDecl"; break;

-			case 132: s = "this symbol not expected in ClassDecl"; break;

-			case 133: s = "this symbol not expected in DatatypeDecl"; break;

-			case 134: s = "invalid DatatypeDecl"; break;

-			case 135: s = "this symbol not expected in DatatypeDecl"; break;

-			case 136: s = "invalid OtherTypeDecl"; break;

-			case 137: s = "invalid OtherTypeDecl"; break;

-			case 138: s = "this symbol not expected in OtherTypeDecl"; break;

-			case 139: s = "this symbol not expected in IteratorDecl"; break;

-			case 140: s = "invalid IteratorDecl"; break;

-			case 141: s = "this symbol not expected in TraitDecl"; break;

-			case 142: s = "invalid ClassMemberDecl"; break;

-			case 143: s = "invalid IdentOrDigitsSuffix"; break;

-			case 144: s = "this symbol not expected in FieldDecl"; break;

-			case 145: s = "this symbol not expected in FieldDecl"; break;

-			case 146: s = "invalid FunctionDecl"; break;

-			case 147: s = "invalid FunctionDecl"; break;

+			case 78: s = "\"new\" expected"; break;

+			case 79: s = "\"[\" expected"; break;

+			case 80: s = "\"]\" expected"; break;

+			case 81: s = "\"if\" expected"; break;

+			case 82: s = "\"else\" expected"; break;

+			case 83: s = "\"case\" expected"; break;

+			case 84: s = "\"while\" expected"; break;

+			case 85: s = "\"invariant\" expected"; break;

+			case 86: s = "\"match\" expected"; break;

+			case 87: s = "\"assert\" expected"; break;

+			case 88: s = "\"print\" expected"; break;

+			case 89: s = "\"forall\" expected"; break;

+			case 90: s = "\"parallel\" expected"; break;

+			case 91: s = "\"modify\" expected"; break;

+			case 92: s = "\"calc\" expected"; break;

+			case 93: s = "\"#\" expected"; break;

+			case 94: s = "\"<=\" expected"; break;

+			case 95: s = "\">=\" expected"; break;

+			case 96: s = "\"!=\" expected"; break;

+			case 97: s = "\"\\u2260\" expected"; break;

+			case 98: s = "\"\\u2264\" expected"; break;

+			case 99: s = "\"\\u2265\" expected"; break;

+			case 100: s = "\"<==>\" expected"; break;

+			case 101: s = "\"\\u21d4\" expected"; break;

+			case 102: s = "\"==>\" expected"; break;

+			case 103: s = "\"\\u21d2\" expected"; break;

+			case 104: s = "\"<==\" expected"; break;

+			case 105: s = "\"\\u21d0\" expected"; break;

+			case 106: s = "\"&&\" expected"; break;

+			case 107: s = "\"\\u2227\" expected"; break;

+			case 108: s = "\"||\" expected"; break;

+			case 109: s = "\"\\u2228\" expected"; break;

+			case 110: s = "\"in\" expected"; break;

+			case 111: s = "\"!\" expected"; break;

+			case 112: s = "\"+\" expected"; break;

+			case 113: s = "\"-\" expected"; break;

+			case 114: s = "\"/\" expected"; break;

+			case 115: s = "\"%\" expected"; break;

+			case 116: s = "\"\\u00ac\" expected"; break;

+			case 117: s = "\"false\" expected"; break;

+			case 118: s = "\"true\" expected"; break;

+			case 119: s = "\"null\" expected"; break;

+			case 120: s = "\"this\" expected"; break;

+			case 121: s = "\"fresh\" expected"; break;

+			case 122: s = "\"old\" expected"; break;

+			case 123: s = "\"then\" expected"; break;

+			case 124: s = "\"..\" expected"; break;

+			case 125: s = "\"\\u2200\" expected"; break;

+			case 126: s = "\"exists\" expected"; break;

+			case 127: s = "\"\\u2203\" expected"; break;

+			case 128: s = "\"::\" expected"; break;

+			case 129: s = "\"\\u2022\" expected"; break;

+			case 130: s = "??? expected"; break;

+			case 131: s = "this symbol not expected in SubModuleDecl"; break;

+			case 132: s = "invalid SubModuleDecl"; break;

+			case 133: s = "this symbol not expected in ClassDecl"; break;

+			case 134: s = "this symbol not expected in DatatypeDecl"; break;

+			case 135: s = "invalid DatatypeDecl"; break;

+			case 136: s = "this symbol not expected in DatatypeDecl"; break;

+			case 137: s = "invalid NewtypeDecl"; break;

+			case 138: s = "this symbol not expected in NewtypeDecl"; break;

+			case 139: s = "invalid OtherTypeDecl"; break;

+			case 140: s = "this symbol not expected in OtherTypeDecl"; break;

+			case 141: s = "this symbol not expected in IteratorDecl"; break;

+			case 142: s = "invalid IteratorDecl"; break;

+			case 143: s = "this symbol not expected in TraitDecl"; break;

+			case 144: s = "invalid ClassMemberDecl"; break;

+			case 145: s = "invalid IdentOrDigitsSuffix"; break;

+			case 146: s = "this symbol not expected in FieldDecl"; break;

+			case 147: s = "this symbol not expected in FieldDecl"; break;

 			case 148: s = "invalid FunctionDecl"; break;

 			case 149: s = "invalid FunctionDecl"; break;

-			case 150: s = "this symbol not expected in MethodDecl"; break;

-			case 151: s = "invalid MethodDecl"; break;

-			case 152: s = "invalid MethodDecl"; break;

-			case 153: s = "invalid FIdentType"; break;

-			case 154: s = "invalid TypeIdentOptional"; break;

-			case 155: s = "invalid TypeAndToken"; break;

-			case 156: s = "this symbol not expected in IteratorSpec"; break;

-			case 157: s = "this symbol not expected in IteratorSpec"; break;

+			case 150: s = "invalid FunctionDecl"; break;

+			case 151: s = "invalid FunctionDecl"; break;

+			case 152: s = "this symbol not expected in MethodDecl"; break;

+			case 153: s = "invalid MethodDecl"; break;

+			case 154: s = "invalid MethodDecl"; break;

+			case 155: s = "invalid FIdentType"; break;

+			case 156: s = "invalid TypeIdentOptional"; break;

+			case 157: s = "invalid TypeAndToken"; break;

 			case 158: s = "this symbol not expected in IteratorSpec"; break;

 			case 159: s = "this symbol not expected in IteratorSpec"; break;

 			case 160: s = "this symbol not expected in IteratorSpec"; break;

-			case 161: s = "invalid IteratorSpec"; break;

+			case 161: s = "this symbol not expected in IteratorSpec"; break;

 			case 162: s = "this symbol not expected in IteratorSpec"; break;

 			case 163: s = "invalid IteratorSpec"; break;

-			case 164: s = "this symbol not expected in MethodSpec"; break;

-			case 165: s = "this symbol not expected in MethodSpec"; break;

+			case 164: s = "this symbol not expected in IteratorSpec"; break;

+			case 165: s = "invalid IteratorSpec"; break;

 			case 166: s = "this symbol not expected in MethodSpec"; break;

 			case 167: s = "this symbol not expected in MethodSpec"; break;

-			case 168: s = "invalid MethodSpec"; break;

+			case 168: s = "this symbol not expected in MethodSpec"; break;

 			case 169: s = "this symbol not expected in MethodSpec"; break;

 			case 170: s = "invalid MethodSpec"; break;

-			case 171: s = "invalid FrameExpression"; break;

-			case 172: s = "invalid ReferenceType"; break;

-			case 173: s = "this symbol not expected in FunctionSpec"; break;

-			case 174: s = "this symbol not expected in FunctionSpec"; break;

+			case 171: s = "this symbol not expected in MethodSpec"; break;

+			case 172: s = "invalid MethodSpec"; break;

+			case 173: s = "invalid FrameExpression"; break;

+			case 174: s = "invalid ReferenceType"; break;

 			case 175: s = "this symbol not expected in FunctionSpec"; break;

 			case 176: s = "this symbol not expected in FunctionSpec"; break;

 			case 177: s = "this symbol not expected in FunctionSpec"; break;

-			case 178: s = "invalid FunctionSpec"; break;

-			case 179: s = "invalid PossiblyWildFrameExpression"; break;

-			case 180: s = "invalid PossiblyWildExpression"; break;

-			case 181: s = "this symbol not expected in OneStmt"; break;

-			case 182: s = "invalid OneStmt"; break;

+			case 178: s = "this symbol not expected in FunctionSpec"; break;

+			case 179: s = "this symbol not expected in FunctionSpec"; break;

+			case 180: s = "invalid FunctionSpec"; break;

+			case 181: s = "invalid PossiblyWildFrameExpression"; break;

+			case 182: s = "invalid PossiblyWildExpression"; break;

 			case 183: s = "this symbol not expected in OneStmt"; break;

 			case 184: s = "invalid OneStmt"; break;

-			case 185: s = "invalid AssertStmt"; break;

-			case 186: s = "invalid AssumeStmt"; break;

-			case 187: s = "invalid UpdateStmt"; break;

-			case 188: s = "invalid UpdateStmt"; break;

-			case 189: s = "invalid IfStmt"; break;

-			case 190: s = "invalid IfStmt"; break;

-			case 191: s = "invalid WhileStmt"; break;

-			case 192: s = "invalid WhileStmt"; break;

-			case 193: s = "invalid MatchStmt"; break;

-			case 194: s = "invalid ForallStmt"; break;

-			case 195: s = "invalid ForallStmt"; break;

-			case 196: s = "this symbol not expected in ModifyStmt"; break;

-			case 197: s = "invalid ModifyStmt"; break;

-			case 198: s = "invalid ReturnStmt"; break;

-			case 199: s = "invalid Rhs"; break;

-			case 200: s = "invalid Lhs"; break;

-			case 201: s = "invalid Guard"; break;

-			case 202: s = "this symbol not expected in LoopSpec"; break;

-			case 203: s = "this symbol not expected in LoopSpec"; break;

+			case 185: s = "this symbol not expected in OneStmt"; break;

+			case 186: s = "invalid OneStmt"; break;

+			case 187: s = "invalid AssertStmt"; break;

+			case 188: s = "invalid AssumeStmt"; break;

+			case 189: s = "invalid UpdateStmt"; break;

+			case 190: s = "invalid UpdateStmt"; break;

+			case 191: s = "invalid IfStmt"; break;

+			case 192: s = "invalid IfStmt"; break;

+			case 193: s = "invalid WhileStmt"; break;

+			case 194: s = "invalid WhileStmt"; break;

+			case 195: s = "invalid MatchStmt"; break;

+			case 196: s = "invalid ForallStmt"; break;

+			case 197: s = "invalid ForallStmt"; break;

+			case 198: s = "this symbol not expected in ModifyStmt"; break;

+			case 199: s = "invalid ModifyStmt"; break;

+			case 200: s = "invalid ReturnStmt"; break;

+			case 201: s = "invalid Rhs"; break;

+			case 202: s = "invalid Lhs"; break;

+			case 203: s = "invalid Guard"; break;

 			case 204: s = "this symbol not expected in LoopSpec"; break;

 			case 205: s = "this symbol not expected in LoopSpec"; break;

 			case 206: s = "this symbol not expected in LoopSpec"; break;

-			case 207: s = "this symbol not expected in Invariant"; break;

-			case 208: s = "invalid AttributeArg"; break;

-			case 209: s = "invalid CalcOp"; break;

-			case 210: s = "invalid EquivOp"; break;

-			case 211: s = "invalid ImpliesOp"; break;

-			case 212: s = "invalid ExpliesOp"; break;

-			case 213: s = "invalid AndOp"; break;

-			case 214: s = "invalid OrOp"; break;

-			case 215: s = "invalid RelOp"; break;

-			case 216: s = "invalid AddOp"; break;

-			case 217: s = "invalid UnaryExpression"; break;

-			case 218: s = "invalid UnaryExpression"; break;

-			case 219: s = "invalid MulOp"; break;

-			case 220: s = "invalid NegOp"; break;

-			case 221: s = "invalid EndlessExpression"; break;

-			case 222: s = "invalid Suffix"; break;

-			case 223: s = "invalid Suffix"; break;

+			case 207: s = "this symbol not expected in LoopSpec"; break;

+			case 208: s = "this symbol not expected in LoopSpec"; break;

+			case 209: s = "this symbol not expected in Invariant"; break;

+			case 210: s = "invalid AttributeArg"; break;

+			case 211: s = "invalid CalcOp"; break;

+			case 212: s = "invalid EquivOp"; break;

+			case 213: s = "invalid ImpliesOp"; break;

+			case 214: s = "invalid ExpliesOp"; break;

+			case 215: s = "invalid AndOp"; break;

+			case 216: s = "invalid OrOp"; break;

+			case 217: s = "invalid RelOp"; break;

+			case 218: s = "invalid AddOp"; break;

+			case 219: s = "invalid UnaryExpression"; break;

+			case 220: s = "invalid UnaryExpression"; break;

+			case 221: s = "invalid MulOp"; break;

+			case 222: s = "invalid NegOp"; break;

+			case 223: s = "invalid EndlessExpression"; break;

 			case 224: s = "invalid Suffix"; break;

-			case 225: s = "invalid DisplayExpr"; break;

-			case 226: s = "invalid MultiSetExpr"; break;

-			case 227: s = "invalid ConstAtomExpression"; break;

-			case 228: s = "invalid Nat"; break;

-			case 229: s = "invalid LambdaArrow"; break;

-			case 230: s = "invalid QSep"; break;

-			case 231: s = "invalid MatchExpression"; break;

-			case 232: s = "invalid QuantifierGuts"; break;

-			case 233: s = "invalid StmtInExpr"; break;

-			case 234: s = "invalid LetExpr"; break;

-			case 235: s = "invalid CasePattern"; break;

-			case 236: s = "invalid Forall"; break;

-			case 237: s = "invalid Exists"; break;

+			case 225: s = "invalid Suffix"; break;

+			case 226: s = "invalid Suffix"; break;

+			case 227: s = "invalid DisplayExpr"; break;

+			case 228: s = "invalid MultiSetExpr"; break;

+			case 229: s = "invalid ConstAtomExpression"; break;

+			case 230: s = "invalid Nat"; break;

+			case 231: s = "invalid LambdaArrow"; break;

+			case 232: s = "invalid QSep"; break;

+			case 233: s = "invalid MatchExpression"; break;

+			case 234: s = "invalid QuantifierGuts"; break;

+			case 235: s = "invalid StmtInExpr"; break;

+			case 236: s = "invalid LetExpr"; break;

+			case 237: s = "invalid CasePattern"; break;

+			case 238: s = "invalid Forall"; break;

+			case 239: s = "invalid Exists"; break;

 

 			default: s = "error " + n; break;

 		}

diff --git a/Source/Dafny/Scanner.cs b/Source/Dafny/Scanner.cs
index a54fe778..df41ffcd 100644
--- a/Source/Dafny/Scanner.cs
+++ b/Source/Dafny/Scanner.cs
@@ -211,8 +211,8 @@ public class UTF8Buffer: Buffer {
 public class Scanner {

 	const char EOL = '\n';

 	const int eofSym = 0; /* pdt */

-	const int maxT = 129;

-	const int noSym = 129;

+	const int maxT = 130;

+	const int noSym = 130;

 

 

 	[ContractInvariantMethod]

@@ -509,59 +509,60 @@ public class Scanner {
 			case "datatype": t.kind = 33; break;

 			case "codatatype": t.kind = 34; break;

 			case "var": t.kind = 36; break;

-			case "type": t.kind = 38; break;

-			case "new": t.kind = 40; break;

-			case "iterator": t.kind = 41; break;

-			case "yields": t.kind = 42; break;

-			case "returns": t.kind = 43; break;

-			case "method": t.kind = 47; break;

-			case "lemma": t.kind = 48; break;

-			case "colemma": t.kind = 49; break;

-			case "comethod": t.kind = 50; break;

-			case "constructor": t.kind = 51; break;

-			case "modifies": t.kind = 52; break;

-			case "free": t.kind = 53; break;

-			case "ensures": t.kind = 54; break;

-			case "decreases": t.kind = 55; break;

-			case "yield": t.kind = 56; break;

-			case "bool": t.kind = 57; break;

-			case "nat": t.kind = 58; break;

-			case "int": t.kind = 59; break;

-			case "real": t.kind = 60; break;

-			case "set": t.kind = 61; break;

-			case "multiset": t.kind = 62; break;

-			case "seq": t.kind = 63; break;

-			case "map": t.kind = 64; break;

-			case "object": t.kind = 65; break;

-			case "function": t.kind = 67; break;

-			case "predicate": t.kind = 68; break;

-			case "copredicate": t.kind = 69; break;

-			case "label": t.kind = 71; break;

-			case "break": t.kind = 72; break;

-			case "where": t.kind = 73; break;

+			case "newtype": t.kind = 38; break;

+			case "where": t.kind = 39; break;

+			case "type": t.kind = 40; break;

+			case "iterator": t.kind = 42; break;

+			case "yields": t.kind = 43; break;

+			case "returns": t.kind = 44; break;

+			case "method": t.kind = 48; break;

+			case "lemma": t.kind = 49; break;

+			case "colemma": t.kind = 50; break;

+			case "comethod": t.kind = 51; break;

+			case "constructor": t.kind = 52; break;

+			case "modifies": t.kind = 53; break;

+			case "free": t.kind = 54; break;

+			case "ensures": t.kind = 55; break;

+			case "decreases": t.kind = 56; break;

+			case "yield": t.kind = 57; break;

+			case "bool": t.kind = 58; break;

+			case "nat": t.kind = 59; break;

+			case "int": t.kind = 60; break;

+			case "real": t.kind = 61; break;

+			case "set": t.kind = 62; break;

+			case "multiset": t.kind = 63; break;

+			case "seq": t.kind = 64; break;

+			case "map": t.kind = 65; break;

+			case "object": t.kind = 66; break;

+			case "function": t.kind = 68; break;

+			case "predicate": t.kind = 69; break;

+			case "copredicate": t.kind = 70; break;

+			case "label": t.kind = 72; break;

+			case "break": t.kind = 73; break;

 			case "return": t.kind = 75; break;

 			case "assume": t.kind = 77; break;

-			case "if": t.kind = 80; break;

-			case "else": t.kind = 81; break;

-			case "case": t.kind = 82; break;

-			case "while": t.kind = 83; break;

-			case "invariant": t.kind = 84; break;

-			case "match": t.kind = 85; break;

-			case "assert": t.kind = 86; break;

-			case "print": t.kind = 87; break;

-			case "forall": t.kind = 88; break;

-			case "parallel": t.kind = 89; break;

-			case "modify": t.kind = 90; break;

-			case "calc": t.kind = 91; break;

-			case "in": t.kind = 109; break;

-			case "false": t.kind = 116; break;

-			case "true": t.kind = 117; break;

-			case "null": t.kind = 118; break;

-			case "this": t.kind = 119; break;

-			case "fresh": t.kind = 120; break;

-			case "old": t.kind = 121; break;

-			case "then": t.kind = 122; break;

-			case "exists": t.kind = 125; break;

+			case "new": t.kind = 78; break;

+			case "if": t.kind = 81; break;

+			case "else": t.kind = 82; break;

+			case "case": t.kind = 83; break;

+			case "while": t.kind = 84; break;

+			case "invariant": t.kind = 85; break;

+			case "match": t.kind = 86; break;

+			case "assert": t.kind = 87; break;

+			case "print": t.kind = 88; break;

+			case "forall": t.kind = 89; break;

+			case "parallel": t.kind = 90; break;

+			case "modify": t.kind = 91; break;

+			case "calc": t.kind = 92; break;

+			case "in": t.kind = 110; break;

+			case "false": t.kind = 117; break;

+			case "true": t.kind = 118; break;

+			case "null": t.kind = 119; break;

+			case "this": t.kind = 120; break;

+			case "fresh": t.kind = 121; break;

+			case "old": t.kind = 122; break;

+			case "then": t.kind = 123; break;

+			case "exists": t.kind = 126; break;

 			default: break;

 		}

 	}

@@ -714,66 +715,66 @@ public class Scanner {
 			case 33:

 				{t.kind = 37; break;}

 			case 34:

-				{t.kind = 44; break;}

+				{t.kind = 45; break;}

 			case 35:

-				{t.kind = 70; break;}

+				{t.kind = 71; break;}

 			case 36:

 				{t.kind = 74; break;}

 			case 37:

 				{t.kind = 76; break;}

 			case 38:

-				{t.kind = 78; break;}

-			case 39:

 				{t.kind = 79; break;}

+			case 39:

+				{t.kind = 80; break;}

 			case 40:

-				{t.kind = 92; break;}

+				{t.kind = 93; break;}

 			case 41:

-				{t.kind = 94; break;}

-			case 42:

 				{t.kind = 95; break;}

-			case 43:

+			case 42:

 				{t.kind = 96; break;}

-			case 44:

+			case 43:

 				{t.kind = 97; break;}

-			case 45:

+			case 44:

 				{t.kind = 98; break;}

-			case 46:

+			case 45:

 				{t.kind = 99; break;}

-			case 47:

+			case 46:

 				{t.kind = 100; break;}

-			case 48:

+			case 47:

 				{t.kind = 101; break;}

-			case 49:

+			case 48:

 				{t.kind = 102; break;}

+			case 49:

+				{t.kind = 103; break;}

 			case 50:

-				{t.kind = 104; break;}

+				{t.kind = 105; break;}

 			case 51:

 				if (ch == '&') {AddCh(); goto case 52;}

 				else {goto case 0;}

 			case 52:

-				{t.kind = 105; break;}

-			case 53:

 				{t.kind = 106; break;}

-			case 54:

+			case 53:

 				{t.kind = 107; break;}

-			case 55:

+			case 54:

 				{t.kind = 108; break;}

+			case 55:

+				{t.kind = 109; break;}

 			case 56:

-				{t.kind = 111; break;}

+				{t.kind = 112; break;}

 			case 57:

-				{t.kind = 113; break;}

-			case 58:

 				{t.kind = 114; break;}

-			case 59:

+			case 58:

 				{t.kind = 115; break;}

+			case 59:

+				{t.kind = 116; break;}

 			case 60:

-				{t.kind = 124; break;}

+				{t.kind = 125; break;}

 			case 61:

-				{t.kind = 126; break;}

-			case 62:

 				{t.kind = 127; break;}

-			case 63:

+			case 62:

 				{t.kind = 128; break;}

+			case 63:

+				{t.kind = 129; break;}

 			case 64:

 				recEnd = pos; recKind = 7;

 				if (ch == '=') {AddCh(); goto case 36;}

@@ -786,46 +787,46 @@ public class Scanner {
 				else if (ch == '=') {AddCh(); goto case 72;}

 				else {t.kind = 25; break;}

 			case 66:

-				recEnd = pos; recKind = 112;

+				recEnd = pos; recKind = 113;

 				if (ch == '>') {AddCh(); goto case 15;}

-				else {t.kind = 112; break;}

+				else {t.kind = 113; break;}

 			case 67:

-				recEnd = pos; recKind = 110;

+				recEnd = pos; recKind = 111;

 				if (ch == 'i') {AddCh(); goto case 21;}

 				else if (ch == '=') {AddCh(); goto case 42;}

-				else {t.kind = 110; break;}

+				else {t.kind = 111; break;}

 			case 68:

 				recEnd = pos; recKind = 35;

 				if (ch == '|') {AddCh(); goto case 54;}

 				else {t.kind = 35; break;}

 			case 69:

-				recEnd = pos; recKind = 66;

+				recEnd = pos; recKind = 67;

 				if (ch == '.') {AddCh(); goto case 73;}

-				else {t.kind = 66; break;}

+				else {t.kind = 67; break;}

 			case 70:

-				recEnd = pos; recKind = 45;

+				recEnd = pos; recKind = 46;

 				if (ch == '=') {AddCh(); goto case 74;}

-				else {t.kind = 45; break;}

+				else {t.kind = 46; break;}

 			case 71:

-				recEnd = pos; recKind = 46;

+				recEnd = pos; recKind = 47;

 				if (ch == '=') {AddCh(); goto case 41;}

-				else {t.kind = 46; break;}

+				else {t.kind = 47; break;}

 			case 72:

-				recEnd = pos; recKind = 39;

+				recEnd = pos; recKind = 41;

 				if (ch == '>') {AddCh(); goto case 48;}

-				else {t.kind = 39; break;}

+				else {t.kind = 41; break;}

 			case 73:

-				recEnd = pos; recKind = 123;

+				recEnd = pos; recKind = 124;

 				if (ch == '.') {AddCh(); goto case 34;}

-				else {t.kind = 123; break;}

+				else {t.kind = 124; break;}

 			case 74:

-				recEnd = pos; recKind = 93;

+				recEnd = pos; recKind = 94;

 				if (ch == '=') {AddCh(); goto case 75;}

-				else {t.kind = 93; break;}

+				else {t.kind = 94; break;}

 			case 75:

-				recEnd = pos; recKind = 103;

+				recEnd = pos; recKind = 104;

 				if (ch == '>') {AddCh(); goto case 46;}

-				else {t.kind = 103; break;}

+				else {t.kind = 104; break;}

 

 		}

 		t.val = new String(tval, 0, tlen);

diff --git a/Source/DafnyExtension/TokenTagger.cs b/Source/DafnyExtension/TokenTagger.cs
index 438d9be6..f54d5184 100644
--- a/Source/DafnyExtension/TokenTagger.cs
+++ b/Source/DafnyExtension/TokenTagger.cs
@@ -320,6 +320,7 @@ namespace DafnyLanguage
                 case "multiset":

                 case "nat":

                 case "new":

+                case "newtype":

                 case "null":

                 case "object":

                 case "old":

@@ -340,6 +341,7 @@ namespace DafnyLanguage
                 case "true":

                 case "type":

                 case "var":

+                case "where":

                 case "while":

                 case "yield":

                 case "yields":

diff --git a/Test/dafny0/DerivedTypes.dfy b/Test/dafny0/DerivedTypes.dfy
index 7a2249da..ef9b7dae 100644
--- a/Test/dafny0/DerivedTypes.dfy
+++ b/Test/dafny0/DerivedTypes.dfy
@@ -1,9 +1,9 @@
 // RUN: %dafny /print:"%t.print" /dprint:"%t.dprint" "%s" > "%t"

 // RUN: %diff "%s.expect" "%t"

 

-type int32 = new int

-type posReal = new real

-type int8 = new int32

+newtype int32 = int

+newtype posReal = real

+newtype int8 = int32

 

 method M()

 {

diff --git a/Test/dafny0/DerivedTypesResolution.dfy b/Test/dafny0/DerivedTypesResolution.dfy
index 336a087a..c3a02eeb 100644
--- a/Test/dafny0/DerivedTypesResolution.dfy
+++ b/Test/dafny0/DerivedTypesResolution.dfy
@@ -3,19 +3,19 @@
 

 module Cycle {

   type MySynonym = MyNewType  // error: a cycle

-  type MyNewType = new MyIntegerType_WellSupposedly

+  newtype MyNewType = MyIntegerType_WellSupposedly

   type MyIntegerType_WellSupposedly = MySynonym

 }

 

 module MustBeNumeric {

   datatype List<T> = Nil | Cons(T, List)

-  type NewDatatype = new List<int>  // error: base type must be numeric based

+  newtype NewDatatype = List<int>  // error: base type must be numeric based

 }

 

 module Goodies {

-  type int32 = new int

-  type posReal = new real

-  type int8 = new int32

+  newtype int32 = int

+  newtype posReal = real

+  newtype int8 = int32

 

   method M()

   {

diff --git a/Test/dafny0/DerivedTypesResolution.dfy.expect b/Test/dafny0/DerivedTypesResolution.dfy.expect
index 4f86c813..6b1c3ae4 100644
--- a/Test/dafny0/DerivedTypesResolution.dfy.expect
+++ b/Test/dafny0/DerivedTypesResolution.dfy.expect
@@ -1,5 +1,5 @@
 DerivedTypesResolution.dfy(5,7): Error: Cycle among redirecting types (derived types, type synonyms): MySynonym -> MyIntegerType_WellSupposedly -> MyNewType -> MySynonym

-DerivedTypesResolution.dfy(12,7): Error: derived types must be based on some numeric type (got List<int>)

+DerivedTypesResolution.dfy(12,10): Error: derived types must be based on some numeric type (got List<int>)

 DerivedTypesResolution.dfy(38,9): Error: arguments must have the same type (got posReal and real)

 DerivedTypesResolution.dfy(44,9): Error: arguments must have the same type (got int32 and int)

 DerivedTypesResolution.dfy(50,13): Error: arguments must have the same type (got posReal and int32)

diff --git a/Util/Emacs/dafny-mode.el b/Util/Emacs/dafny-mode.el
index d589fb78..6482ff28 100644
--- a/Util/Emacs/dafny-mode.el
+++ b/Util/Emacs/dafny-mode.el
@@ -30,7 +30,7 @@
 ]\\)*" . font-lock-comment-face)

 

    `(,(dafny-regexp-opt '(

-        "class" "datatype" "codatatype" "type" "iterator"

+        "class" "datatype" "codatatype" "newtype" "type" "iterator"

 	"trait" "extends"

         "function" "predicate" "copredicate"

         "ghost" "var" "method" "lemma" "constructor" "colemma"

diff --git a/Util/latex/dafny.sty b/Util/latex/dafny.sty
index 40b994ba..dc0d18c7 100644
--- a/Util/latex/dafny.sty
+++ b/Util/latex/dafny.sty
@@ -5,7 +5,7 @@
 \usepackage{listings}

 

 \lstdefinelanguage{dafny}{

-  morekeywords={class,datatype,codatatype,type,iterator,trait,extends,

+  morekeywords={class,datatype,codatatype,newtype,type,iterator,trait,extends,

       bool,nat,int,real,object,set,multiset,seq,array,array2,array3,map,

       function,predicate,copredicate,

       ghost,var,static,refines,

diff --git a/Util/vim/dafny.vim b/Util/vim/dafny.vim
index 58820c0f..92c0b079 100644
--- a/Util/vim/dafny.vim
+++ b/Util/vim/dafny.vim
@@ -7,7 +7,7 @@ syntax clear
 syntax case match
 syntax keyword dafnyFunction function predicate copredicate
 syntax keyword dafnyMethod method lemma constructor colemma
-syntax keyword dafnyTypeDef class datatype codatatype type iterator trait extends
+syntax keyword dafnyTypeDef class datatype codatatype newtype type iterator trait extends
 syntax keyword dafnyModule abstract module import opened as default
 syntax keyword dafnyConditional if then else match case
 syntax keyword dafnyRepeat while