Update tla-io/src/main/scala/at/forsyte/apalache/io/quint/Quint.scala

Co-authored-by: Gabriela Moreira <gabrielamoreiramafra@gmail.com>
apalache-mc · Dec 1, 2023 · 2f52f8e · 2f52f8e
1 parent 8fe7379
commit 2f52f8e
Showing 1 changed file with 2 additions and 2 deletions.
diff --git a/tla-io/src/main/scala/at/forsyte/apalache/io/quint/Quint.scala b/tla-io/src/main/scala/at/forsyte/apalache/io/quint/Quint.scala
@@ -422,9 +422,9 @@ class Quint(quintOutput: QuintOutput) {
     //
     // This is converted into the following Apalache expression, using Apalache's variant operators:
     //
-    // CASE VariantTag(expr) = "F1" -> elim_1(VariantGetUnsafe(expr))
+    // CASE VariantTag(expr) = "F1" -> elim_1(VariantGetUnsafe("F1", expr))
     //   [] ...
-    //   [] VariantTag(expr) = "Fn" -> elim_n(VariantGetUnsafe(expr))
+    //   [] VariantTag(expr) = "Fn" -> elim_n(VariantGetUnsafe("Fn", expr))
     //
     // This ensures that we will apply the proper eliminator to the expected value
     // associated with whatever tag is carried by the variant `expr`.