diff options
| author |  Rustan Leino <leino@microsoft.com> | 2012-01-10 13:23:20 -0800 |
|---|---|---|
| committer | Rustan Leino <leino@microsoft.com> | 2012-01-10 13:23:20 -0800 |
| commit | ae8ba23b193e160d0e6363558482a8f955034775 (patch) | |
| tree | 070689560ebef9cdf7168dc3ffecc5993bc928c0 /Util/VS2010 | |
| parent | 8973c639509884d7493e1fe3f70bf3b0de8fa277 (diff) | |
Dafny: added predicates
Diffstat (limited to 'Util/VS2010')
| -rw-r--r-- | Util/VS2010/Dafny/DafnyLanguageService/Grammar.cs | 3 | ||||
| -rw-r--r-- | Util/VS2010/DafnyExtension/DafnyExtension/TokenTagger.cs | 1 |
2 files changed, 3 insertions, 1 deletions
diff --git a/Util/VS2010/Dafny/DafnyLanguageService/Grammar.cs b/Util/VS2010/Dafny/DafnyLanguageService/Grammar.cs index e35383b0..41923a98 100644 --- a/Util/VS2010/Dafny/DafnyLanguageService/Grammar.cs +++ b/Util/VS2010/Dafny/DafnyLanguageService/Grammar.cs @@ -24,7 +24,7 @@ namespace Demo "break", "label", "return", "parallel", "havoc", "print",
"returns", "requires", "ensures", "modifies", "reads", "decreases",
"bool", "nat", "int", "false", "true", "null",
- "function", "free",
+ "function", "predicate", "free",
"in", "forall", "exists",
"seq", "set", "multiset", "array", "array2", "array3",
"match", "case",
@@ -301,6 +301,7 @@ namespace Demo | "true"
| "null"
| "function"
+ | "predicate"
| "free"
| "in"
| "forall"
diff --git a/Util/VS2010/DafnyExtension/DafnyExtension/TokenTagger.cs b/Util/VS2010/DafnyExtension/DafnyExtension/TokenTagger.cs index 78c5f8d9..650c01bd 100644 --- a/Util/VS2010/DafnyExtension/DafnyExtension/TokenTagger.cs +++ b/Util/VS2010/DafnyExtension/DafnyExtension/TokenTagger.cs @@ -272,6 +272,7 @@ namespace DafnyLanguage case "object":
case "old":
case "parallel":
+ case "predicate":
case "print":
case "reads":
case "refines":
|