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/OpaqueFunctions.dfy | |
| parent | 9ee34997bf0787ce4aaee1fafc475e0728bec61d (diff) | |
New logical encoding of types with Is and IsAlloc
Diffstat (limited to 'Test/dafny0/OpaqueFunctions.dfy')
| -rw-r--r-- | Test/dafny0/OpaqueFunctions.dfy | 7 |
1 files changed, 6 insertions, 1 deletions
diff --git a/Test/dafny0/OpaqueFunctions.dfy b/Test/dafny0/OpaqueFunctions.dfy index d95a6160..3b591ef2 100644 --- a/Test/dafny0/OpaqueFunctions.dfy +++ b/Test/dafny0/OpaqueFunctions.dfy @@ -157,4 +157,9 @@ module M1 refines M0 { // ---------------------------------- opaque and generics
-function{:opaque} zero<A>():int { 0 }
+function{:opaque} id<A>(x : A):A { x }
+
+datatype Box<A> = Bx(A)
+
+function{:opaque} id_box(x : Box):Box { x }
+
|