From 9aac1a22c4ff4b4be16800b86e34a94d358b0deb Mon Sep 17 00:00:00 2001
From: adelon <22380201+adelon@users.noreply.github.com>
Date: Wed, 16 Jul 2025 12:36:32 +0200
Subject: Add quantified calcs and relax tokenization

Use an `\iff`-calc to speed up `union_as_unions`. Also remove `in_implies_neq` which seems to interact badly with the choice axiom used by superposition-based proofs like Vampire in cut-down problems.
---
 test/golden/calc/glossing.golden | 4 ++--
 test/golden/calc/parsing.golden  | 4 ++--
 2 files changed, 4 insertions(+), 4 deletions(-)

(limited to 'test/golden/calc')

diff --git a/test/golden/calc/glossing.golden b/test/golden/calc/glossing.golden
index 96366d4..ed4f3c0 100644
--- a/test/golden/calc/glossing.golden
+++ b/test/golden/calc/glossing.golden
@@ -71,7 +71,7 @@
         , sourceColumn = Pos 1
         }
     )
-    ( Calc
+    ( Calc CalcUnquantified
         ( Equation
             ( TermVar
                 ( NamedVar "y" )
@@ -120,7 +120,7 @@
         , sourceColumn = Pos 1
         }
     )
-    ( Calc
+    ( Calc CalcUnquantified
         ( Biconditionals
             ( TermSymbol
                 ( SymbolPredicate
diff --git a/test/golden/calc/parsing.golden b/test/golden/calc/parsing.golden
index 3d86683..b6f393a 100644
--- a/test/golden/calc/parsing.golden
+++ b/test/golden/calc/parsing.golden
@@ -80,7 +80,7 @@
         , sourceColumn = Pos 1
         }
     )
-    ( Calc
+    ( Calc Nothing
         ( Equation
             ( ExprVar
                 ( NamedVar "y" )
@@ -132,7 +132,7 @@
         , sourceColumn = Pos 1
         }
     )
-    ( Calc
+    ( Calc Nothing
         ( Biconditionals
             ( FormulaChain
                 ( ChainBase
-- 
cgit v1.2.3