diff options
author | Rustan Leino <leino@microsoft.com> | 2011-04-20 23:51:33 -0700 |
---|---|---|
committer | Rustan Leino <leino@microsoft.com> | 2011-04-20 23:51:33 -0700 |
commit | ec5c7538c19c214bd76d2004b55abf7cf3c6b0b3 (patch) | |
tree | 1be73fcf3f1f120f3fe7938069a44f252bd52d1d /Util | |
parent | 5bd736fee46b289c130110fdf5cad91aa97d9475 (diff) |
Dafny: Alternative (and candidate replacement) syntax for declaring datatypes
Dafny: Additional induction test cases
Diffstat (limited to 'Util')
-rw-r--r-- | Util/VS2010/Dafny/DafnyLanguageService/Grammar.cs | 17 |
1 files changed, 3 insertions, 14 deletions
diff --git a/Util/VS2010/Dafny/DafnyLanguageService/Grammar.cs b/Util/VS2010/Dafny/DafnyLanguageService/Grammar.cs index 3302d368..a9353821 100644 --- a/Util/VS2010/Dafny/DafnyLanguageService/Grammar.cs +++ b/Util/VS2010/Dafny/DafnyLanguageService/Grammar.cs @@ -178,6 +178,7 @@ namespace Demo | "=" | "+=" | "-="
| "."
| "==>" | "<==>" | "<<"
+ | "=" // this is for datatype declarations, not an operator
;
LUnOp.Rule = ToTerm("-") | "~" | "!";
@@ -349,6 +350,7 @@ namespace Demo | ","
| ":"
| ";"
+ | "=" // this is for datatype declarations, not an operator
| "."
| "`"
| "=="
@@ -435,20 +437,7 @@ namespace Demo #endregion
#region 5. Operators precedence
- RegisterOperators(1, "<==>");
- RegisterOperators(2, "+", "-");
- RegisterOperators(3, "*", "/", "%", "!!");
- RegisterOperators(4, Associativity.Right, "^");
- RegisterOperators(5, "||");
- RegisterOperators(6, "&&");
- RegisterOperators(7, "==", "!=", ">", "<", ">=", "<=");
- RegisterOperators(8, "in");
- RegisterOperators(9, "-", "!", "++", "--");
- RegisterOperators(10, "==>");
- RegisterOperators(11, ".");
-
- //RegisterOperators(10, Associativity.Right, ".",",", ")", "(", "]", "[", "{", "}");
- //RegisterOperators(11, Associativity.Right, "else");
+ // not used
#endregion
#region 6. Punctuation symbols
|