diff options
Diffstat (limited to 'Source/Dafny/Dafny.atg')
| -rw-r--r-- | Source/Dafny/Dafny.atg | 7 |
1 files changed, 5 insertions, 2 deletions
diff --git a/Source/Dafny/Dafny.atg b/Source/Dafny/Dafny.atg index 5fa1085d..ff3b75a3 100644 --- a/Source/Dafny/Dafny.atg +++ b/Source/Dafny/Dafny.atg @@ -2175,10 +2175,13 @@ ImpliesExpliesExpression<out Expression e0, bool allowSemi, bool allowLambda> ( ImpliesOp (. x = t; .)
ImpliesExpression<out e1, allowSemi, allowLambda> (. e0 = new BinaryExpr(x, BinaryExpr.Opcode.Imp, e0, e1); .)
| ExpliesOp (. x = t; .)
- LogicalExpression<out e1, allowSemi, allowLambda> (. e0 = new BinaryExpr(x, BinaryExpr.Opcode.Exp, e0, e1); .)
+ LogicalExpression<out e1, allowSemi, allowLambda> (. // The order of operands is reversed so that it can be turned into implication during resolution
+ e0 = new BinaryExpr(x, BinaryExpr.Opcode.Exp, e1, e0); .)
{ IF(IsExpliesOp()) /* read a reverse implication as far as possible */
ExpliesOp (. x = t; .)
- LogicalExpression<out e1, allowSemi, allowLambda> (. e0 = new BinaryExpr(x, BinaryExpr.Opcode.Exp, e0, e1); .)
+ LogicalExpression<out e1, allowSemi, allowLambda> (. //The order of operands is reversed so that it can be turned into implication during resolution
+ e0 = new BinaryExpr(x, BinaryExpr.Opcode.Exp, e1, e0);
+ .)
}
)
]
|