Update assets/src/semantics-of-regular-expressions/Languages.dfy

Co-authored-by: Rustan Leino <[email protected]>
dafny-lang · Jan 3, 2024 · edd1018 · edd1018
1 parent 62227be
commit edd1018
Showing 1 changed file with 3 additions and 1 deletion.
diff --git a/assets/src/semantics-of-regular-expressions/Languages.dfy b/assets/src/semantics-of-regular-expressions/Languages.dfy
@@ -177,7 +177,9 @@ module Languages {
     requires Bisimilar(L1, L2)
     ensures Bisimilar(Star(L1), Star(L2))
   {
-    forall k ensures Bisimilar#[k](Star(L1), Star(L2)) {
+    forall k: nat
+      ensures Bisimilar#[k](Star(L1), Star(L2))
+    {
       if k != 0 {
         var k' :| k' + 1 == k;
         StarCongruenceHelper(k', L1, L2);