Skip to content
Snippets Groups Projects
Commit 5b313dca authored by Katja Goltsova's avatar Katja Goltsova Committed by Viktor Kunčak
Browse files

Change parser tests because ' has been disallowed in names

parent 2644c177
No related branches found
No related tags found
No related merge requests found
......@@ -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))
)
}
}
0% Loading or .
You are about to add 0 people to the discussion. Proceed with caution.
Please register or to comment