New logical encoding of types with Is and IsAlloc

1 files changed, 3 insertions, 3 deletions

diff --git a/Test/dafny0/NoTypeArgs.dfy b/Test/dafny0/NoTypeArgs.dfy
index a97d63a3..d658af78 100644
--- a/Test/dafny0/NoTypeArgs.dfy
+++ b/Test/dafny0/NoTypeArgs.dfy
@@ -73,14 +73,14 @@ ghost method Theorem(xs: List)
   }

 }

 

-ghost method Lemma(xs: List, ys: List)

+ghost method Lemma<A>(xs: List, ys: List)

   ensures reverse(concat(xs, ys)) == concat(reverse(ys), reverse(xs));

 {

   match (xs) {

     case Nil =>

-      assert forall ws :: concat(ws, Nil) == ws;

+      assert forall ws :: concat(ws, Nil) == var ws : List<A> := ws; ws;

     case Cons(t, rest) =>

-      assert forall a, b, c :: concat(a, concat(b, c)) == concat(concat(a, b), c);

+      assert forall a, b, c :: concat(a, concat(b, c)) == var ws : List <A> := concat(concat(a, b), c); ws;

   }

 }