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.
---
 source/Syntax/Token.hs | 13 ++++++++-----
 1 file changed, 8 insertions(+), 5 deletions(-)

(limited to 'source/Syntax/Token.hs')

diff --git a/source/Syntax/Token.hs b/source/Syntax/Token.hs
index 53e1e6a..2dad049 100644
--- a/source/Syntax/Token.hs
+++ b/source/Syntax/Token.hs
@@ -321,14 +321,17 @@ var = guardM isMathMode *> lexeme (fmap Variable var')
     where
     var' = do
         alphabeticPart <- letter <|> bb <|> greek
-        variationPart  <- subscriptNumber <|> ticked <|> pure ""
+        variationPart  <- subscript <|> ticked <|> pure ""
         pure (alphabeticPart <> variationPart)
 
-    subscriptNumber :: Lexer Text
-    subscriptNumber = do
+    subscript :: Lexer Text
+    subscript = do
         Char.char '_'
-        n <- some Char.digitChar
-        pure (Text.pack n)
+        unbraced <|> braced <|> text
+        where
+            unbraced = Text.singleton <$> Char.alphaNumChar
+            braced = Text.pack <$> (Char.char '{' *> many Char.alphaNumChar <* Char.char '}')
+            text = Char.string "\\text" *> braced -- for rendering the subscript in roman type
 
     -- Temporary hack to fit the TPTP format.
     ticked :: Lexer Text
-- 
cgit v1.2.3