From 5b313dca83756d4fada68df8c57c6aa005a0d997 Mon Sep 17 00:00:00 2001
From: Katja Goltsova <katja.goltsova@protonmail.com>
Date: Wed, 5 Oct 2022 16:37:04 +0200
Subject: [PATCH] Change parser tests because ' has been disallowed in names
---
lisa-utils/src/test/scala/lisa/utils/ParserTest.scala | 6 +++---
1 file changed, 3 insertions(+), 3 deletions(-)
diff --git a/lisa-utils/src/test/scala/lisa/utils/ParserTest.scala b/lisa-utils/src/test/scala/lisa/utils/ParserTest.scala
index 6717983e..c4373935 100644
--- a/lisa-utils/src/test/scala/lisa/utils/ParserTest.scala
+++ b/lisa-utils/src/test/scala/lisa/utils/ParserTest.scala
@@ -213,10 +213,10 @@ class ParserTest extends AnyFunSuite with TestUtils {
)
assert(Parser.parseSequent("⊢ ('x = 'x) ∨ ('x = 'y)") == (() |- (x === x) \/ (x === y)))
assert(
- Parser.parseSequent("('x = 'x) ∨ ('x = 'y); ('x = 'x) ∨ ('x = 'y) ↔ ('x = 'x') ∨ ('x = 'y') ⊢ ('x = 'x') ∨ ('x = 'y')") == (Set(
+ Parser.parseSequent("('x = 'x) ∨ ('x = 'y); ('x = 'x) ∨ ('x = 'y) ↔ ('x = 'x1) ∨ ('x = 'y1) ⊢ ('x = 'x1) ∨ ('x = 'y1)") == (Set(
(x === x) \/ (x === y),
- ((x === x) \/ (x === y)) <=> ((x === xPrime) \/ (x === yPrime))
- ) |- (x === xPrime) \/ (x === yPrime))
+ ((x === x) \/ (x === y)) <=> ((x === x1) \/ (x === y1))
+ ) |- (x === x1) \/ (x === y1))
)
}
}
--
GitLab