diff options
author | Dan Rosén <danr@chalmers.se> | 2014-07-10 16:52:09 -0700 |
---|---|---|
committer | Dan Rosén <danr@chalmers.se> | 2014-07-10 16:52:09 -0700 |
commit | 92cced2f7bde488e450fa12f7ef50d98f474ab61 (patch) | |
tree | d9cc893bc1289d8ad09b21f6a2242d31fa51ef70 /Test/dafny0/OpaqueFunctionsFail.dfy | |
parent | 129ab22811996b4b46cfbcc6eb3f4b97a95f5416 (diff) |
Make reveal axioms from opaque functions quantify over layers
Diffstat (limited to 'Test/dafny0/OpaqueFunctionsFail.dfy')
-rw-r--r-- | Test/dafny0/OpaqueFunctionsFail.dfy | 6 |
1 files changed, 3 insertions, 3 deletions
diff --git a/Test/dafny0/OpaqueFunctionsFail.dfy b/Test/dafny0/OpaqueFunctionsFail.dfy index ae7f81f6..3895ed3c 100644 --- a/Test/dafny0/OpaqueFunctionsFail.dfy +++ b/Test/dafny0/OpaqueFunctionsFail.dfy @@ -1,9 +1,9 @@ - -// ---------------------------------- opaque and generics - // RUN: %dafny /compile:0 /print:"%t.print" /dprint:"%t.dprint" "%s" > "%t" // RUN: %diff "%s.expect" "%t" + +// ---------------------------------- opaque and generics + // This function cannot normally be called, so the // generated opaquity code contains such a bad call. function{:opaque} zero<A>():int { 0 } |