diff options
| -rw-r--r-- | Binaries/DafnyPrelude.bpl | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/Binaries/DafnyPrelude.bpl b/Binaries/DafnyPrelude.bpl index 5ee8b845..ef6106e0 100644 --- a/Binaries/DafnyPrelude.bpl +++ b/Binaries/DafnyPrelude.bpl @@ -836,7 +836,7 @@ function Seq#Contains<T>(Seq T, T): bool; axiom (forall<T> s: Seq T, x: T :: { Seq#Contains(s,x) }
Seq#Contains(s,x) <==>
(exists i: int :: { Seq#Index(s,i) } 0 <= i && i < Seq#Length(s) && Seq#Index(s,i) == x));
-axiom (forall x: ref ::
+axiom (forall<T> x: T ::
{ Seq#Contains(Seq#Empty(), x) }
!Seq#Contains(Seq#Empty(), x));
|