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 21b895aa..4c761671 100644 --- a/Test/dafny1/Celebrity.dfy +++ b/Test/dafny1/Celebrity.dfy @@ -10,7 +10,7 @@ static function IsCelebrity<Person>(c: Person, people: set<Person>): bool }
method FindCelebrity0<Person>(people: set<Person>, ghost c: Person) returns (r: Person)
- requires (exists c :: IsCelebrity(c, people));
+ requires exists c :: IsCelebrity(c, people);
ensures r == c;
{
var cc; assume cc == c; // this line essentially converts ghost c to non-ghost cc
|