blob: a1b155aca41867d6fbc09d4a33015c8c2b020c7e (
plain)
1
2
3
4
5
6
7
8
|
// RUN: %dafny /compile:0 /print:"%t.print" /dprint:"%t.dprint" "%s" > "%t"
// RUN: %diff "%s.expect" "%t"
function domain<U, V>(m: imap<U,V>): set<U>
ensures forall i :: i in domain(m) <==> i in m;
{
set s | s in m // UNSAFE, m may have infinite domain
}
|
