diff options
Diffstat (limited to 'Test/hofs/TreeMapSimple.dfy')
| -rw-r--r-- | Test/hofs/TreeMapSimple.dfy | 6 |
1 files changed, 3 insertions, 3 deletions
diff --git a/Test/hofs/TreeMapSimple.dfy b/Test/hofs/TreeMapSimple.dfy index 3ba4ffd6..e717b096 100644 --- a/Test/hofs/TreeMapSimple.dfy +++ b/Test/hofs/TreeMapSimple.dfy @@ -1,4 +1,4 @@ -// RUN: %dafny /compile:0 "%s" > "%t" +// RUN: %dafny "%s" > "%t" // RUN: %diff "%s.expect" "%t" datatype List<A> = Nil | Cons(head: A,tail: List<A>); @@ -27,7 +27,7 @@ function Pre(f : A -> B, s : set<A>) : bool } function method Map(xs : List<A>, f : A -> B): List<B> - reads (set x, y | x in ListData(xs) && y in f.reads(x) :: y); + reads Pre.reads(f, ListData(xs)); requires Pre(f, ListData(xs)); decreases xs; { @@ -37,7 +37,7 @@ function method Map(xs : List<A>, f : A -> B): List<B> } function method TMap(t0 : Tree<A>, f : A -> B) : Tree<B> - reads (set x, y | x in TreeData(t0) && y in f.reads(x) :: y); + reads Pre.reads(f, TreeData(t0)); requires Pre(f, TreeData(t0)); decreases t0; { |