summaryrefslogtreecommitdiff
path: root/Test/dafny0
diff options
context:
space:
mode:
authorGravatar Clément Pit--Claudel <clement.pitclaudel@live.com>2015-08-20 12:49:11 -0700
committerGravatar Clément Pit--Claudel <clement.pitclaudel@live.com>2015-08-20 12:49:11 -0700
commit5734c8b39065b73835092fc5ede4a7c589374be2 (patch)
treece43eb7340e857c0a0b342c9e4486168b7339c9a /Test/dafny0
parent4b7ef1b817fe00bc32294b75797e7e264e2edbdd (diff)
parent270b34fc36dcfc781e8f49df5339cb2e10e69828 (diff)
Merge.
Diffstat (limited to 'Test/dafny0')
-rw-r--r--Test/dafny0/ISets.dfy5
1 files changed, 4 insertions, 1 deletions
diff --git a/Test/dafny0/ISets.dfy b/Test/dafny0/ISets.dfy
index bb0230f4..703039c8 100644
--- a/Test/dafny0/ISets.dfy
+++ b/Test/dafny0/ISets.dfy
@@ -4,7 +4,7 @@
ghost method M()
{
ghost var s := iset{2};
- // test "in
+ // test "in"
if(2 in s)
{
}
@@ -35,6 +35,9 @@ ghost method m1() {
assert s2 - s3 == iset{3}; // set difference
assert (iset x | x in s2 :: x+1) == iset{2,3,4}; // set comprehension
+ assert 17 in (iset x: int | true :: x); // set comprehension
+
+ assert (imap x: int | true :: x+1)[14] == 15;
}