bug

dafny-lang · stefan-aws · Jan 12, 2024 · Dec 14, 2023 · Dec 14, 2023 · Dec 14, 2023
commit 06294c17f0972115aed6f59b1f1e6ece9b632d59
diff --git a/_posts/2024-01-10-semantics-of-regular-expressions.markdown b/_posts/2024-01-10-semantics-of-regular-expressions.markdown
@@ -122,7 +122,7 @@ predicate Bisimilar#<A(!new)>[k: nat](L1: Lang, L2: Lang)
 Now that we have its definition in place, let us establish a property about bisimilarity, say, that it is a [*reflexive*](https://en.wikipedia.org/wiki/Reflexive_relation) relation. With the [`greatest lemma`](https://dafny.org/latest/DafnyRef/DafnyRef#sec-colemmas) construct, Dafny is able to able to derive a proof completely on its own:
 
 ```
-greatest lemma BisimilarityIsReflexive<A>[nat](L: Lang)
+greatest lemma BisimilarityIsReflexive<A(!new)>[nat](L: Lang)
  ensures Bisimilar(L, L)
 {}
 ```

diff --git a/assets/src/semantics-of-regular-expressions/Languages.dfy b/assets/src/semantics-of-regular-expressions/Languages.dfy
@@ -37,7 +37,7 @@ module Languages {
 
  /* Bisimilarity */
 
- greatest lemma BisimilarityIsReflexive<A>[nat](L: Lang)
+ greatest lemma BisimilarityIsReflexive<A(!new)>[nat](L: Lang)
  ensures Bisimilar(L, L)
  {}