diff options
| author |  Dan Rosén <danr@chalmers.se> | 2014-07-07 15:09:33 -0700 |
|---|---|---|
| committer | Dan Rosén <danr@chalmers.se> | 2014-07-07 15:09:33 -0700 |
| commit | 60208673a25423e378cc7e9672d5acf9fd6f58bc (patch) | |
| tree | 32d97449302d4af7fb274825985b2d9c8d9ba008 /Test/dafny0/Modules1.dfy | |
| parent | 9ee34997bf0787ce4aaee1fafc475e0728bec61d (diff) | |
New logical encoding of types with Is and IsAlloc
Diffstat (limited to 'Test/dafny0/Modules1.dfy')
| -rw-r--r-- | Test/dafny0/Modules1.dfy | 6 |
1 files changed, 3 insertions, 3 deletions
diff --git a/Test/dafny0/Modules1.dfy b/Test/dafny0/Modules1.dfy index c4e12780..2f38e39e 100644 --- a/Test/dafny0/Modules1.dfy +++ b/Test/dafny0/Modules1.dfy @@ -122,10 +122,10 @@ module Q_M { abstract module Regression {
module A
{
- predicate p(m: map)
+ predicate p<c,d>(m: map<c,d>)
- lemma m(m: map)
- ensures exists m :: p(m);
+ lemma m<a,b>(m: map<a,b>)
+ ensures exists m :: p(var m : map<a,b> := m; m);
}
abstract module B
|