diff options
Diffstat (limited to 'Test/dafny0/SmallTests.dfy')
| -rw-r--r-- | Test/dafny0/SmallTests.dfy | 17 |
1 files changed, 17 insertions, 0 deletions
diff --git a/Test/dafny0/SmallTests.dfy b/Test/dafny0/SmallTests.dfy index 5fabe354..914e228e 100644 --- a/Test/dafny0/SmallTests.dfy +++ b/Test/dafny0/SmallTests.dfy @@ -518,3 +518,20 @@ class AttributeTests { }
}
}
+
+// ----------------------- Pretty printing of !(!expr) --------
+
+static method TestNotNot()
+{
+ assert !(!true); // Shouldn't pretty print as "!!true".
+
+ assert !(true == false);
+
+ assert !(if true then false else false);
+
+ assert !if true then false else false;
+
+ assert !if !(!true) then false else false;
+
+ assert true == !(!true);
+}
|