diff options
| author |  Bryan Parno <parno@microsoft.com> | 2014-01-23 21:14:19 -0800 |
|---|---|---|
| committer | Bryan Parno <parno@microsoft.com> | 2014-01-23 21:14:19 -0800 |
| commit | 6c322e2e171ffd46b90981ee28119c2dfb9cd121 (patch) | |
| tree | 70f99769a5f6daf5754fbaec16875dd47b880fe3 /Test/dafny0/OpaqueFunctions.dfy | |
| parent | b32bb33052367346817bb8cc6b50943a9ee61c4d (diff) | |
Fix a bug in the interaction between opaque and generics
Diffstat (limited to 'Test/dafny0/OpaqueFunctions.dfy')
| -rw-r--r-- | Test/dafny0/OpaqueFunctions.dfy | 4 |
1 files changed, 4 insertions, 0 deletions
diff --git a/Test/dafny0/OpaqueFunctions.dfy b/Test/dafny0/OpaqueFunctions.dfy index 6bff4ef3..d1e27b90 100644 --- a/Test/dafny0/OpaqueFunctions.dfy +++ b/Test/dafny0/OpaqueFunctions.dfy @@ -151,3 +151,7 @@ module M0 { }
module M1 refines M0 {
}
+
+// ---------------------------------- opaque and generics
+
+function{:opaque} zero<A>():int { 0 }
|