From 166c105b43515bfdbde52514fa9c16ffd61eea25 Mon Sep 17 00:00:00 2001 From: Rustan Leino Date: Mon, 21 Nov 2011 22:40:44 -0800 Subject: Dafny: Added "type" declaration (syntax: "type X;"), which introduces an arbitrary type (like a global type parameter). In the future, a refined module may allow such types to be instantiated. --- Util/VS2010/Dafny/DafnyLanguageService/Grammar.cs | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) (limited to 'Util/VS2010/Dafny') diff --git a/Util/VS2010/Dafny/DafnyLanguageService/Grammar.cs b/Util/VS2010/Dafny/DafnyLanguageService/Grammar.cs index 557beb32..f2924420 100644 --- a/Util/VS2010/Dafny/DafnyLanguageService/Grammar.cs +++ b/Util/VS2010/Dafny/DafnyLanguageService/Grammar.cs @@ -17,7 +17,7 @@ namespace Demo StringLiteral stringLiteral = TerminalFactory.CreateCSharpString("String"); this.MarkReservedWords( // NOTE: these keywords must also appear once more below - "class", "ghost", "static", "var", "method", "constructor", "datatype", + "class", "ghost", "static", "var", "method", "constructor", "datatype", "type", "assert", "assume", "new", "this", "object", "refines", "replaces", "by", "unlimited", "module", "imports", "if", "then", "else", "while", "invariant", @@ -267,6 +267,7 @@ namespace Demo | "method" | "constructor" | "datatype" + | "type" | "assert" | "assume" | "new" -- cgit v1.2.3