diff options
| author |  Rustan Leino <leino@microsoft.com> | 2013-01-16 19:33:15 -0800 |
|---|---|---|
| committer | Rustan Leino <leino@microsoft.com> | 2013-01-16 19:33:15 -0800 |
| commit | 678f36ea920b1be7c7633b9ab7a50672ad54c7b4 (patch) | |
| tree | bccb63f1141697ca3fb57654bafef704eaf0b54f /Source/Dafny/Compiler.cs | |
| parent | b47707c222e2d68fb27d4ace45f106e34b2b9f7f (diff) | |
Removed the syntactic form copredicate #-form with the implicit argument.
Added syntactic support for codatatype #-form equalities.
Diffstat (limited to 'Source/Dafny/Compiler.cs')
| -rw-r--r-- | Source/Dafny/Compiler.cs | 3 |
1 files changed, 3 insertions, 0 deletions
diff --git a/Source/Dafny/Compiler.cs b/Source/Dafny/Compiler.cs index 4b59682f..03d89683 100644 --- a/Source/Dafny/Compiler.cs +++ b/Source/Dafny/Compiler.cs @@ -2174,6 +2174,9 @@ namespace Microsoft.Dafny { wr.Write(")");
}
+ } else if (expr is TernaryExpr) {
+ Contract.Assume(false); // currently, none of the ternary expressions is compilable
+
} else if (expr is LetExpr) {
var e = (LetExpr)expr;
// The Dafny "let" expression
|