diff options
Diffstat (limited to 'Test/dafny1/Substitution.dfy')
| -rw-r--r-- | Test/dafny1/Substitution.dfy | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/Test/dafny1/Substitution.dfy b/Test/dafny1/Substitution.dfy index d3e0e82e..11c8c878 100644 --- a/Test/dafny1/Substitution.dfy +++ b/Test/dafny1/Substitution.dfy @@ -99,7 +99,7 @@ static ghost method TheoremSeq(e: Expression, v: int, val: int) }
}
-static ghost method LemmaSeq(ghost parent: Expression, ghost q: seq<Expression>, v: int, val: int)
+static ghost method LemmaSeq(parent: Expression, q: seq<Expression>, v: int, val: int)
requires (forall a :: a in q ==> a < parent);
ensures |SubstSeq(parent, q, v, val)| == |q|;
ensures (forall k :: 0 <= k && k < |q| ==>
|