diff options
| author |  leino <unknown> | 2014-08-02 01:05:17 -0700 |
|---|---|---|
| committer | leino <unknown> | 2014-08-02 01:05:17 -0700 |
| commit | ae578ae92040975fed005d045110679e4e858c31 (patch) | |
| tree | 79f2a3a67c8c9059a89d9771e933c8a0b6b601bf /Test/dafny0/TypeSynonyms.dfy | |
| parent | 54b670417f5974c43ef2fd55d37ba3806ad5c72d (diff) | |
Fixed bug Issue 37: expand type synonyms in more (hopefully all) places in the resolver and translator
Diffstat (limited to 'Test/dafny0/TypeSynonyms.dfy')
| -rw-r--r-- | Test/dafny0/TypeSynonyms.dfy | 7 |
1 files changed, 7 insertions, 0 deletions
diff --git a/Test/dafny0/TypeSynonyms.dfy b/Test/dafny0/TypeSynonyms.dfy index 4bec5253..85beb340 100644 --- a/Test/dafny0/TypeSynonyms.dfy +++ b/Test/dafny0/TypeSynonyms.dfy @@ -44,3 +44,10 @@ function Skip(s: Synonym3): Synonym0 case Nil => Nil
case Cons(_, tail) => tail
}
+
+type MyMap = map<int, map<real, bool>>
+
+predicate MyMapProperty(m: MyMap, x: int)
+{
+ x in m && real(x) in m[x] && m[x][real(x)]
+}
|