diff options
Diffstat (limited to 'Test/dafny1/Celebrity.dfy')
| -rw-r--r-- | Test/dafny1/Celebrity.dfy | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/Test/dafny1/Celebrity.dfy b/Test/dafny1/Celebrity.dfy index eed06bb1..77af9327 100644 --- a/Test/dafny1/Celebrity.dfy +++ b/Test/dafny1/Celebrity.dfy @@ -4,7 +4,7 @@ method Pick<T>(S: set<T>) returns (t: T); requires S != {};
ensures t in S;
-static function Knows<Person>(a: Person, b: Person): bool;
+static function method Knows<Person>(a: Person, b: Person): bool;
requires a != b; // forbid asking about the reflexive case
static function IsCelebrity<Person>(c: Person, people: set<Person>): bool
|