Dafny: Alternative (and candidate replacement) syntax for declaring datatypes

Dafny: Additional induction test cases

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