blob: 1c3fcf61856d8f358bb43b1915ad07a863cc534d (
plain)
1
2
3
4
5
6
7
8
9
10
|
// RUN: %dafny /compile:0 "%s" > "%t"
// RUN: %diff "%s.expect" "%t"
function{:opaque} MapSetToSet<X, Y>(xs:set<X>, f:X->Y):set<Y>
//function MapSetToSet<X, Y>(xs:set<X>, f:X->Y):set<Y>
reads f.reads;
requires forall x :: f.requires(x);
{
set x | x in xs :: f(x)
}
|
