diff options
author | Rustan Leino <unknown> | 2014-02-13 21:10:16 -0800 |
---|---|---|
committer | Rustan Leino <unknown> | 2014-02-13 21:10:16 -0800 |
commit | 79610237eba7902e8be127fa54f2572a2c01f6b7 (patch) | |
tree | 4c273b46c76e2128cc9e058aebdb96d0c6405bc2 /Source/Dafny/DafnyAst.cs | |
parent | 6897d8be8a9c5ebef140398f682021acfea393bb (diff) |
Allow unary minus on reals
Diffstat (limited to 'Source/Dafny/DafnyAst.cs')
-rw-r--r-- | Source/Dafny/DafnyAst.cs | 15 |
1 files changed, 15 insertions, 0 deletions
diff --git a/Source/Dafny/DafnyAst.cs b/Source/Dafny/DafnyAst.cs index ba05d6a8..f29242ab 100644 --- a/Source/Dafny/DafnyAst.cs +++ b/Source/Dafny/DafnyAst.cs @@ -5642,6 +5642,21 @@ namespace Microsoft.Dafny { }
}
+ /// <summary>
+ /// A NegationExpression e represents the value -e and is syntactic shorthand
+ /// for 0-e (for integers) or 0.0-e (for reals).
+ /// </summary>
+ public class NegationExpression : ConcreteSyntaxExpression
+ {
+ public readonly Expression E;
+ public NegationExpression(IToken tok, Expression e)
+ : base(tok) {
+ Contract.Requires(tok != null);
+ Contract.Requires(e != null);
+ E = e;
+ }
+ }
+
public class ChainingExpression : ConcreteSyntaxExpression
{
public readonly List<Expression> Operands;
|