Allow relation symbols with parameters

Parameters must follow the relation symbol and be surrounded by braces, like so: `\rel{x}{y}{z}`.

This attempt is still brittle/broken in a few ways:
- It makes using braces in creative ways in mixfix notation ambiguous.
- It does not verify that the parameters are used in a consistent manner for each symbol. It essentially allows users to define  `a\MyRel b` and `a\MyRel{x} b` (and ones with even more parameters).
- It allows parameters for all relation symbols, even for those where it makes no sense in ordinary TeX markup, e.g. `a <{x} b`.

23 files changed, 159 insertions, 146 deletions

diff --git a/library/topology/urysohntwo.tex b/library/topology/urysohntwo.tex
index eda3c32..7f69aa4 100644
--- a/library/topology/urysohntwo.tex
+++ b/library/topology/urysohntwo.tex
@@ -473,7 +473,7 @@
 \begin{proof}[Proof by \in-induction on $n$]
     Assume $n \in \naturals$.
     Suppose $Y$ has cardinality $n$.
-    $X$ has cardinality $n$ by \cref{bijection_converse_is_bijection,bijection_circ,regularity,cardinality,foundation,empty_eq,emptyset}.
+    $X$ has cardinality $n$ by \cref{bijection_converse_is_bijection,bijection_circ,regularity,cardinality,foundation,emptyset}.
     \begin{byCase}
         \caseOf{$n = \zero$.}
             Follows by \cref{converse_converse_eq,injective_converse_is_function,converse_is_relation,dom_converse,id_is_function_to,id_ran,ran_circ_exact,circ,ran_converse,emptyset_is_function_on_emptyset,bijective_converse_are_funs,relext,function_member_elim,bijection_is_function,cardinality,bijections_dom,in_irrefl,codom_of_emptyset_can_be_anything,converse_emptyset,funs_elim,neq_witness,id}.
diff --git a/source/Meaning.hs b/source/Meaning.hs
index 3822221..61f1d7b 100644
--- a/source/Meaning.hs
+++ b/source/Meaning.hs
@@ -42,6 +42,7 @@ type Gloss = ExceptT GlossError (State GlossState)
 data GlossError
     = GlossDefnError DefnError String
     | GlossInductionError
+    | GlossRelationExprWithParams
     deriving (Show, Eq, Ord)
 
 
@@ -189,36 +190,39 @@ glossChain :: Sem.Chain -> Gloss (Sem.ExprOf VarSymbol)
 glossChain ch = Sem.makeConjunction <$> makeRels (conjuncts (splat ch))
     where
         -- | Separate each link of the chain into separate triples.
-        splat :: Raw.Chain -> [(NonEmpty Raw.Expr, Sign, Raw.Relation, NonEmpty Raw.Expr)]
+        splat :: Raw.Chain -> [(NonEmpty Raw.Expr, Sign, Raw.Relation, [Raw.Expr], NonEmpty Raw.Expr)]
         splat = \case
-            Raw.ChainBase es sign rel es'
-                -> [(es, sign, rel, es')]
-            Raw.ChainCons es sign rel ch'@(Raw.ChainBase es' _ _ _)
-                -> (es, sign, rel, es') : splat ch'
-            Raw.ChainCons es sign rel ch'@(Raw.ChainCons es' _ _ _)
-                -> (es, sign, rel, es') : splat ch'
+            Raw.ChainBase es sign rel params es'
+                -> [(es, sign, rel, params, es')]
+            Raw.ChainCons es sign rel params ch'@(Raw.ChainBase es' _ _ _ _)
+                -> (es, sign, rel, params, es') : splat ch'
+            Raw.ChainCons es sign rel params ch'@(Raw.ChainCons es' _ _ _ _)
+                -> (es, sign, rel, params, es') : splat ch'
 
         -- | Take each triple and combine the lhs/rhs to make all the conjuncts.
-        conjuncts :: [(NonEmpty Raw.Expr, Sign, Raw.Relation, NonEmpty Raw.Expr)] -> [(Sign, Raw.Relation, Raw.Expr, Raw.Expr)]
+        conjuncts :: [(NonEmpty Raw.Expr, Sign, Raw.Relation, [Raw.Expr], NonEmpty Raw.Expr)] -> [(Sign, Raw.Relation, [Raw.Expr], Raw.Expr, Raw.Expr)]
         conjuncts triples = do
-            (e1s, sign, rel, e2s) <- triples
+            (e1s, sign, rel, params, e2s) <- triples
             e1 <- toList e1s
             e2 <- toList e2s
-            pure (sign, rel, e1, e2)
+            pure (sign, rel, params, e1, e2)
 
-        makeRels :: [(Sign, Raw.Relation, Raw.Expr, Raw.Expr)] -> Gloss [Sem.Formula]
+        makeRels :: [(Sign, Raw.Relation, [Raw.Expr], Raw.Expr, Raw.Expr)] -> Gloss [Sem.Formula]
         makeRels triples = for triples makeRel
 
-        makeRel :: (Sign, Raw.Relation, Raw.Expr, Raw.Expr) -> Gloss Sem.Formula
-        makeRel (sign, rel, e1, e2) = do
+        makeRel :: (Sign, Raw.Relation, [Raw.Expr], Raw.Expr, Raw.Expr) -> Gloss Sem.Formula
+        makeRel (sign, rel, params, e1, e2) = do
             e1' <- glossExpr e1
             e2' <- glossExpr e2
+            params' <- glossExpr `each` params
             case rel of
                 Raw.RelationSymbol tok ->
-                    pure $ sign' $ Sem.Relation tok (e1' : [e2'])
-                Raw.RelationExpr e -> do
-                    e' <- glossExpr e
-                    pure $ sign' $ Sem.TermPair e1' e2' `Sem.IsElementOf` e'
+                    pure $ sign' $ Sem.Relation tok (params' <> [e1',e2'])
+                Raw.RelationExpr e -> case params of
+                        [] -> do
+                            e' <- glossExpr e
+                            pure (sign' (Sem.TermPair e1' e2' `Sem.IsElementOf` e'))
+                        _ -> throwError GlossRelationExprWithParams
             where
                 sign' = case sign of
                     Positive -> id
@@ -542,8 +546,12 @@ glossDefnHead = \case
         pure $ \asms f -> Sem.DefnPredicate asms (Sem.PredicateVerb verb) (v :| vs) f
     Raw.DefnNoun v (Raw.Noun noun vs) ->
         pure $ \asms f -> Sem.DefnPredicate asms (Sem.PredicateNoun noun) (v :| vs) f
-    Raw.DefnRel v1 rel v2 ->
-        pure $ \asms f -> Sem.DefnPredicate asms (Sem.PredicateRelation rel) (v1 :| [v2]) f
+    Raw.DefnRel v1 rel params v2 ->
+        pure \asms f ->
+            let args = case params of
+                    p : ps -> p :| (ps <> [v1, v2])
+                    [] -> v1 :| [v2]
+            in Sem.DefnPredicate asms (Sem.PredicateRelation rel) args f
     Raw.DefnSymbolicPredicate (Raw.PrefixPredicate symb _ar) vs ->
         pure $ \asms f -> Sem.DefnPredicate asms (Sem.PredicateSymbol symb) vs f
 
@@ -688,8 +696,8 @@ glossAbbreviation = \case
         makeAbbrStmt (Sem.SymbolPredicate (Sem.PredicateVerb verb)) (x : xs) stmt
     Raw.AbbreviationNoun x (Raw.Noun noun xs) stmt ->
         makeAbbrStmt (Sem.SymbolPredicate (Sem.PredicateNoun noun)) (x : xs) stmt
-    Raw.AbbreviationRel x rel y stmt ->
-        makeAbbrStmt (Sem.SymbolPredicate (Sem.PredicateRelation rel)) [x, y] stmt
+    Raw.AbbreviationRel x rel params y stmt ->
+        makeAbbrStmt (Sem.SymbolPredicate (Sem.PredicateRelation rel)) (params <> [x, y]) stmt
     Raw.AbbreviationFun (Raw.Fun fun xs) t ->
         makeAbbrTerm (Sem.SymbolFun fun) xs t
     Raw.AbbreviationEq (Raw.SymbolPattern op xs) e ->
diff --git a/source/Syntax/Abstract.hs b/source/Syntax/Abstract.hs
index 23da652..31a1029 100644
--- a/source/Syntax/Abstract.hs
+++ b/source/Syntax/Abstract.hs
@@ -92,8 +92,8 @@ makeTuple = foldr1 ExprPair
 
 
 data Chain
-    = ChainBase (NonEmpty Expr) Sign Relation (NonEmpty Expr)
-    | ChainCons (NonEmpty Expr) Sign Relation Chain
+    = ChainBase (NonEmpty Expr) Sign Relation [Expr] (NonEmpty Expr) -- left arguments, possibly empty list of parameters, right arguments
+    | ChainCons (NonEmpty Expr) Sign Relation [Expr] Chain
     deriving (Show, Eq, Ord)
 
 data Relation
@@ -319,7 +319,7 @@ data DefnHead
     | DefnVerb (Maybe (NounPhrase Maybe)) VarSymbol (VerbOf VarSymbol)
     | DefnNoun VarSymbol (NounOf VarSymbol)
     | DefnSymbolicPredicate PrefixPredicate (NonEmpty VarSymbol)
-    | DefnRel VarSymbol RelationSymbol VarSymbol
+    | DefnRel VarSymbol RelationSymbol [VarSymbol] VarSymbol
     -- ^ E.g.: /@$x \subseteq y$ iff [...@/
     deriving (Show, Eq, Ord)
 
@@ -411,7 +411,7 @@ data Abbreviation
     = AbbreviationAdj VarSymbol (AdjOf VarSymbol) Stmt
     | AbbreviationVerb VarSymbol (VerbOf VarSymbol) Stmt
     | AbbreviationNoun VarSymbol (NounOf VarSymbol) Stmt
-    | AbbreviationRel VarSymbol RelationSymbol VarSymbol Stmt
+    | AbbreviationRel VarSymbol RelationSymbol [VarSymbol] VarSymbol Stmt
     | AbbreviationFun (FunOf VarSymbol) Term
     | AbbreviationEq SymbolPattern Expr
     deriving (Show, Eq, Ord)
diff --git a/source/Syntax/Adapt.hs b/source/Syntax/Adapt.hs
index b338d47..1b5a237 100644
--- a/source/Syntax/Adapt.hs
+++ b/source/Syntax/Adapt.hs
@@ -124,7 +124,7 @@ head = ScanNoun <$> noun
     <|> ScanAdj <$> adj
     <|> ScanVerb <$> verb
     <|> ScanFun <$> fun
-    <|> ScanRelationSymbol <$> relationSymbol
+    <|> ScanRelationSymbol . fst <$> relationSymbol
     <|> ScanFunctionSymbol <$> functionSymbol
     <|> ScanPrefixPredicate <$> prefixPredicate
 
@@ -184,14 +184,19 @@ verb = toLexicalPhrase <$> (var *> pat <* iff)
 fun :: RE Token LexicalPhrase
 fun = toLexicalPhrase <$> (the *> pat <* (is <|> comma))
 
-relationSymbol :: RE Token RelationSymbol
-relationSymbol = math relator' <* iff
+relationSymbol :: RE Token (RelationSymbol, Int)
+relationSymbol = definiendum <* iff
     where
-        relator' = do
+        definiendum = math do
             varSymbol
             rel <- symbol
+            k <- params
             varSymbol
-            pure rel
+            pure (rel, k)
+        params :: RE Token Int
+        params = do
+            vars <- many (sym InvisibleBraceL *> var <* sym InvisibleBraceR)
+            pure (length vars)
 
 functionSymbol :: RE Token FunctionSymbol
 functionSymbol = do
diff --git a/source/Syntax/Concrete.hs b/source/Syntax/Concrete.hs
index 383f348..3c6700b 100644
--- a/source/Syntax/Concrete.hs
+++ b/source/Syntax/Concrete.hs
@@ -84,8 +84,8 @@ grammar lexicon@Lexicon{..} = mdo
     relationSign   <- rule $ pure Positive <|> (Negative <$ command "not")
     relationExpr   <- rule $ RelationExpr <$> (command "mathrel" *> group expr)
     relation       <- rule $ (RelationSymbol <$> relator) <|> relationExpr
-    chainBase      <- rule $ ChainBase <$> exprs <*> relationSign <*> relation <*> exprs
-    chainCons      <- rule $ ChainCons <$> exprs <*> relationSign <*> relation <*> chain
+    chainBase      <- rule $ ChainBase <$> exprs <*> relationSign <*> relation <*> many (brace expr) <*> exprs
+    chainCons      <- rule $ ChainCons <$> exprs <*> relationSign <*> relation <*> many (brace expr) <*> chain
     chain          <- rule $ chainCons <|> chainBase
 
     formulaPredicate  <- rule $ asum $ prefixPredicateOf FormulaPredicate expr <$> HM.keys lexiconPrefixPredicates
@@ -250,7 +250,7 @@ grammar lexicon@Lexicon{..} = mdo
     defnAdj <- rule $ DefnAdj <$> optional (_an *> nounPhrase) <*> var <* _is <*> adjVar
     defnVerb <- rule $ DefnVerb <$> optional (_an *> nounPhrase) <*> var <*> verbVar
     defnNoun <- rule $ DefnNoun <$> var <* _is <* _an <*> nounVar
-    defnRel <- rule $ DefnRel <$> (beginMath *> varSymbol) <*> relator <*> varSymbol <* endMath
+    defnRel <- rule $ DefnRel <$> (beginMath *> varSymbol) <*> relator <*> many (group varSymbol) <*> varSymbol <* endMath
     defnSymbolicPredicate <- rule $ math $ asum $ prefixPredicateOf DefnSymbolicPredicate varSymbol <$> HM.keys lexiconPrefixPredicates
     defnHead <- rule $ optional _write *> asum [defnAdj, defnVerb, defnNoun, defnRel, defnSymbolicPredicate]
 
@@ -269,7 +269,7 @@ grammar lexicon@Lexicon{..} = mdo
     abbreviationVerb  <- rule $ AbbreviationVerb <$> var <*> verbVar <* (_iff <|> _if) <*> stmt <* _dot
     abbreviationAdj   <- rule $ AbbreviationAdj <$> var <* _is <*> adjVar <* (_iff <|> _if) <*> stmt <* _dot
     abbreviationNoun  <- rule $ AbbreviationNoun <$>  var <* _is <* _an <*> nounVar <* (_iff <|> _if) <*> stmt <* _dot
-    abbreviationRel   <- rule $ AbbreviationRel <$> (beginMath *> varSymbol) <*> relator <*> varSymbol <* endMath <* (_iff <|> _if) <*> stmt <* _dot
+    abbreviationRel   <- rule $ AbbreviationRel <$> (beginMath *> varSymbol) <*> relator <*> many (brace varSymbol) <*> varSymbol <* endMath <* (_iff <|> _if) <*> stmt <* _dot
     abbreviationFun   <- rule $ AbbreviationFun <$> (_the *> funVar) <* (_is <|> _denotes) <*> term <* _dot
     abbreviationEq    <- rule $ uncurry AbbreviationEq <$> symbolicPatternEqTerm
     abbreviation      <- rule $ (abbreviationVerb <|> abbreviationAdj <|> abbreviationNoun <|> abbreviationRel <|> abbreviationFun <|> abbreviationEq)
diff --git a/source/Syntax/Lexicon.hs b/source/Syntax/Lexicon.hs
index 4fe8730..7f79294 100644
--- a/source/Syntax/Lexicon.hs
+++ b/source/Syntax/Lexicon.hs
@@ -112,7 +112,7 @@ prefixOps =
     , ([Just (Command "pow"), Just InvisibleBraceL, Nothing, Just InvisibleBraceR], (NonAssoc, "pow"))
     , ([Just (Command "neg"), Just InvisibleBraceL, Nothing, Just InvisibleBraceR], (NonAssoc, "neg"))
     , ([Just (Command "inv"), Just InvisibleBraceL, Nothing, Just InvisibleBraceR], (NonAssoc, "inv"))
-    , ([Just (Command "abs"), Just InvisibleBraceL, Nothing, Just InvisibleBraceR], (NonAssoc, "abs"))    
+    , ([Just (Command "abs"), Just InvisibleBraceL, Nothing, Just InvisibleBraceR], (NonAssoc, "abs"))
     , (ConsSymbol, (NonAssoc, "cons"))
     , (PairSymbol, (NonAssoc, "pair"))
     -- NOTE Is now defined and hence no longer necessary , (ApplySymbol, (NonAssoc, "apply"))
diff --git a/test/golden/abbr/parsing.golden b/test/golden/abbr/parsing.golden
index 2bc8148..77a4c47 100644
--- a/test/golden/abbr/parsing.golden
+++ b/test/golden/abbr/parsing.golden
@@ -24,7 +24,7 @@
                             ) Positive
                             ( RelationSymbol
                                 ( Command "in" )
-                            )
+                            ) []
                             ( ExprVar
                                 ( NamedVar "x" ) :| []
                             )
@@ -105,7 +105,7 @@
                     ) Positive
                     ( RelationSymbol
                         ( Symbol "=" )
-                    )
+                    ) []
                     ( ExprVar
                         ( NamedVar "x" ) :| []
                     )
@@ -181,7 +181,7 @@
                     ) Positive
                     ( RelationSymbol
                         ( Symbol "=" )
-                    )
+                    ) []
                     ( ExprVar
                         ( NamedVar "y" ) :| []
                     )
@@ -240,7 +240,7 @@
                         ) Positive
                         ( RelationSymbol
                             ( Symbol "=" )
-                        )
+                        ) []
                         ( ExprVar
                             ( NamedVar "y" ) :| []
                         )
@@ -267,7 +267,7 @@
                         ) Positive
                         ( RelationSymbol
                             ( Command "notin" )
-                        )
+                        ) []
                         ( ExprVar
                             ( NamedVar "y" ) :| []
                         )
@@ -282,7 +282,7 @@
                         ) Negative
                         ( RelationSymbol
                             ( Command "in" )
-                        )
+                        ) []
                         ( ExprVar
                             ( NamedVar "y" ) :| []
                         )
@@ -340,7 +340,7 @@
                         ) Positive
                         ( RelationSymbol
                             ( Command "in" )
-                        )
+                        ) []
                         ( ExprVar
                             ( NamedVar "y" ) :| []
                         )
@@ -396,7 +396,7 @@
                         ) Positive
                         ( RelationSymbol
                             ( Symbol "=" )
-                        )
+                        ) []
                         ( ExprVar
                             ( NamedVar "y" ) :| []
                         )
diff --git a/test/golden/byRef/parsing.golden b/test/golden/byRef/parsing.golden
index 3df8730..e7e3287 100644
--- a/test/golden/byRef/parsing.golden
+++ b/test/golden/byRef/parsing.golden
@@ -15,7 +15,7 @@
                     ) Positive
                     ( RelationSymbol
                         ( Symbol "=" )
-                    )
+                    ) []
                     ( ExprVar
                         ( NamedVar "a" ) :| []
                     )
@@ -40,7 +40,7 @@
                     ) Positive
                     ( RelationSymbol
                         ( Symbol "=" )
-                    )
+                    ) []
                     ( ExprVar
                         ( NamedVar "b" ) :| []
                     )
@@ -65,7 +65,7 @@
                     ) Positive
                     ( RelationSymbol
                         ( Symbol "=" )
-                    )
+                    ) []
                     ( ExprVar
                         ( NamedVar "c" ) :| []
                     )
@@ -102,7 +102,7 @@
                     ) Positive
                     ( RelationSymbol
                         ( Symbol "=" )
-                    )
+                    ) []
                     ( ExprVar
                         ( NamedVar "e" ) :| []
                     )
@@ -128,7 +128,7 @@
                         ) Positive
                         ( RelationSymbol
                             ( Symbol "=" )
-                        )
+                        ) []
                         ( ExprVar
                             ( NamedVar "d" ) :| []
                         )
@@ -157,7 +157,7 @@
                     ) Positive
                     ( RelationSymbol
                         ( Symbol "=" )
-                    )
+                    ) []
                     ( ExprVar
                         ( NamedVar "f" ) :| []
                     )
diff --git a/test/golden/calc/parsing.golden b/test/golden/calc/parsing.golden
index b6f393a..89997b4 100644
--- a/test/golden/calc/parsing.golden
+++ b/test/golden/calc/parsing.golden
@@ -15,7 +15,7 @@
                     ) Positive
                     ( RelationSymbol
                         ( Symbol "=" )
-                    )
+                    ) []
                     ( ExprVar
                         ( NamedVar "x" ) :| []
                     )
@@ -40,7 +40,7 @@
                     ) Positive
                     ( RelationSymbol
                         ( Symbol "=" )
-                    )
+                    ) []
                     ( ExprVar
                         ( NamedVar "z" ) :| []
                     )
@@ -65,7 +65,7 @@
                     ) Positive
                     ( RelationSymbol
                         ( Symbol "=" )
-                    )
+                    ) []
                     ( ExprVar
                         ( NamedVar "y" ) :| []
                     )
@@ -117,7 +117,7 @@
                     ) Positive
                     ( RelationSymbol
                         ( Symbol "=" )
-                    )
+                    ) []
                     ( ExprVar
                         ( NamedVar "y" ) :| []
                     )
@@ -141,7 +141,7 @@
                     ) Positive
                     ( RelationSymbol
                         ( Symbol "=" )
-                    )
+                    ) []
                     ( ExprVar
                         ( NamedVar "y" ) :| []
                     )
@@ -159,7 +159,7 @@
                             ) Positive
                             ( RelationSymbol
                                 ( Symbol "=" )
-                            )
+                            ) []
                             ( ExprVar
                                 ( NamedVar "y" ) :| []
                             )
diff --git a/test/golden/coord/parsing.golden b/test/golden/coord/parsing.golden
index 65fa82f..a2b6657 100644
--- a/test/golden/coord/parsing.golden
+++ b/test/golden/coord/parsing.golden
@@ -31,7 +31,7 @@
                     ) Positive
                     ( RelationSymbol
                         ( Symbol "=" )
-                    )
+                    ) []
                     ( ExprVar
                         ( NamedVar "x" ) :| []
                     )
@@ -64,7 +64,7 @@
                     ) Positive
                     ( RelationSymbol
                         ( Symbol "=" )
-                    )
+                    ) []
                     ( ExprVar
                         ( NamedVar "x" ) :| []
                     )
@@ -97,7 +97,7 @@
                     ) Positive
                     ( RelationSymbol
                         ( Symbol "=" )
-                    )
+                    ) []
                     ( ExprVar
                         ( NamedVar "x" ) :| []
                     )
@@ -140,7 +140,7 @@
                     ) Positive
                     ( RelationSymbol
                         ( Symbol "=" )
-                    )
+                    ) []
                     ( ExprVar
                         ( NamedVar "x" ) :| []
                     )
@@ -190,7 +190,7 @@
                     ) Positive
                     ( RelationSymbol
                         ( Symbol "=" )
-                    )
+                    ) []
                     ( ExprVar
                         ( NamedVar "x" ) :| []
                     )
@@ -265,7 +265,7 @@
                     ) Positive
                     ( RelationSymbol
                         ( Symbol "=" )
-                    )
+                    ) []
                     ( ExprVar
                         ( NamedVar "x" ) :| []
                     )
@@ -291,7 +291,7 @@
                         ) Positive
                         ( RelationSymbol
                             ( Symbol "=" )
-                        )
+                        ) []
                         ( ExprVar
                             ( NamedVar "y" ) :| []
                         )
diff --git a/test/golden/finite-set-terms/parsing.golden b/test/golden/finite-set-terms/parsing.golden
index c30f70b..e255c8d 100644
--- a/test/golden/finite-set-terms/parsing.golden
+++ b/test/golden/finite-set-terms/parsing.golden
@@ -16,7 +16,7 @@
                         ) Positive
                         ( RelationSymbol
                             ( Command "in" )
-                        )
+                        ) []
                         ( ExprOp
                             [ Just
                                 ( Command "cons" )
@@ -45,7 +45,7 @@
                             ) Positive
                             ( RelationSymbol
                                 ( Symbol "=" )
-                            )
+                            ) []
                             ( ExprVar
                                 ( NamedVar "y" ) :| []
                             )
@@ -60,7 +60,7 @@
                             ) Positive
                             ( RelationSymbol
                                 ( Command "in" )
-                            )
+                            ) []
                             ( ExprVar
                                 ( NamedVar "X" ) :| []
                             )
@@ -111,7 +111,7 @@
                     ) Positive
                     ( RelationSymbol
                         ( Command "in" )
-                    )
+                    ) []
                     ( ExprOp
                         [ Just
                             ( Command "unit" )
diff --git a/test/golden/formula/parsing.golden b/test/golden/formula/parsing.golden
index 7de1fb7..4012bde 100644
--- a/test/golden/formula/parsing.golden
+++ b/test/golden/formula/parsing.golden
@@ -20,7 +20,7 @@
                             ) Positive
                             ( RelationSymbol
                                 ( Symbol "=" )
-                            )
+                            ) []
                             ( ExprVar
                                 ( NamedVar "x" ) :| []
                             )
@@ -33,7 +33,7 @@
                             ) Positive
                             ( RelationSymbol
                                 ( Symbol "=" )
-                            )
+                            ) []
                             ( ExprVar
                                 ( NamedVar "y" ) :| []
                             )
@@ -64,7 +64,7 @@
                         ) Positive
                         ( RelationSymbol
                             ( Symbol "=" )
-                        )
+                        ) []
                         ( ExprVar
                             ( NamedVar "y" ) :| []
                         )
@@ -95,7 +95,7 @@
                             ) Positive
                             ( RelationSymbol
                                 ( Symbol "=" )
-                            )
+                            ) []
                             ( ExprVar
                                 ( NamedVar "y" ) :| []
                             )
@@ -114,7 +114,7 @@
                                 ) Positive
                                 ( RelationSymbol
                                     ( Command "neq" )
-                                )
+                                ) []
                                 ( ExprVar
                                     ( NamedVar "x" ) :| []
                                 )
diff --git a/test/golden/geometry/parsing.golden b/test/golden/geometry/parsing.golden
index b57f76c..1d067d0 100644
--- a/test/golden/geometry/parsing.golden
+++ b/test/golden/geometry/parsing.golden
@@ -244,7 +244,7 @@
                         ) Positive
                         ( RelationSymbol
                             ( Symbol "=" )
-                        )
+                        ) []
                         ( ExprVar
                             ( NamedVar "b" ) :| []
                         )
@@ -516,7 +516,7 @@
                             ) Positive
                             ( RelationSymbol
                                 ( Command "neq" )
-                            )
+                            ) []
                             ( ExprVar
                                 ( NamedVar "b" ) :| []
                             )
@@ -590,7 +590,7 @@
                         ) Positive
                         ( RelationSymbol
                             ( Symbol "=" )
-                        )
+                        ) []
                         ( ExprVar
                             ( NamedVar "b" ) :| []
                         )
@@ -798,7 +798,7 @@
                                     ) Positive
                                     ( RelationSymbol
                                         ( Command "neq" )
-                                    )
+                                    ) []
                                     ( ExprVar
                                         ( NamedVar "v" ) :| []
                                     )
diff --git a/test/golden/inductive/parsing.golden b/test/golden/inductive/parsing.golden
index 7438daa..6d5c0e3 100644
--- a/test/golden/inductive/parsing.golden
+++ b/test/golden/inductive/parsing.golden
@@ -9,7 +9,7 @@
     ( Defn []
         ( DefnRel
             ( NamedVar "A" )
-            ( Command "subseteq" )
+            ( Command "subseteq" ) []
             ( NamedVar "B" )
         )
         ( StmtFormula
@@ -20,7 +20,7 @@
                     ) Positive
                     ( RelationSymbol
                         ( Symbol "=" )
-                    )
+                    ) []
                     ( ExprVar
                         ( NamedVar "B" ) :| []
                     )
@@ -176,7 +176,7 @@
                     ) Positive
                     ( RelationSymbol
                         ( Command "in" )
-                    )
+                    ) []
                     ( ExprOp
                         [ Just
                             ( Command "emptyset" )
@@ -224,7 +224,7 @@
                     ) Positive
                     ( RelationSymbol
                         ( Command "in" )
-                    )
+                    ) []
                     ( ExprOp
                         [ Just
                             ( Command "fin" )
@@ -247,7 +247,7 @@
                             ) Positive
                             ( RelationSymbol
                                 ( Command "in" )
-                            )
+                            ) []
                             ( ExprVar
                                 ( NamedVar "A" ) :| []
                             )
@@ -259,7 +259,7 @@
                             ) Positive
                             ( RelationSymbol
                                 ( Command "in" )
-                            )
+                            ) []
                             ( ExprOp
                                 [ Just
                                     ( Command "fin" )
@@ -293,7 +293,7 @@
                         ) Positive
                         ( RelationSymbol
                             ( Command "in" )
-                        )
+                        ) []
                         ( ExprOp
                             [ Just
                                 ( Command "fin" )
@@ -345,7 +345,7 @@
                         ) Positive
                         ( RelationSymbol
                             ( Command "subseteq" )
-                        )
+                        ) []
                         ( ExprVar
                             ( NamedVar "B" ) :| []
                         )
@@ -369,7 +369,7 @@
                     ) Positive
                     ( RelationSymbol
                         ( Command "subseteq" )
-                    )
+                    ) []
                     ( ExprOp
                         [ Just
                             ( Command "fin" )
@@ -438,7 +438,7 @@
                         ) Positive
                         ( RelationSymbol
                             ( Command "in" )
-                        )
+                        ) []
                         ( ExprVar
                             ( NamedVar "R" ) :| []
                         )
@@ -451,7 +451,7 @@
                     ) Positive
                     ( RelationSymbol
                         ( Command "in" )
-                    )
+                    ) []
                     ( ExprOp
                         [ Just
                             ( Command "tracl" )
@@ -487,7 +487,7 @@
                             ) Positive
                             ( RelationSymbol
                                 ( Command "in" )
-                            )
+                            ) []
                             ( ExprOp
                                 [ Just
                                     ( Command "tracl" )
@@ -520,7 +520,7 @@
                             ) Positive
                             ( RelationSymbol
                                 ( Command "in" )
-                            )
+                            ) []
                             ( ExprVar
                                 ( NamedVar "R" ) :| []
                             )
@@ -546,7 +546,7 @@
                         ) Positive
                         ( RelationSymbol
                             ( Command "in" )
-                        )
+                        ) []
                         ( ExprOp
                             [ Just
                                 ( Command "tracl" )
@@ -616,7 +616,7 @@
                         ) Positive
                         ( RelationSymbol
                             ( Command "in" )
-                        )
+                        ) []
                         ( ExprOp
                             [ Just
                                 ( Command "fld" )
@@ -650,7 +650,7 @@
                     ) Positive
                     ( RelationSymbol
                         ( Command "in" )
-                    )
+                    ) []
                     ( ExprOp
                         [ Just
                             ( Command "qrefltracl" )
@@ -686,7 +686,7 @@
                             ) Positive
                             ( RelationSymbol
                                 ( Command "in" )
-                            )
+                            ) []
                             ( ExprOp
                                 [ Just
                                     ( Command "qrefltracl" )
@@ -719,7 +719,7 @@
                             ) Positive
                             ( RelationSymbol
                                 ( Command "in" )
-                            )
+                            ) []
                             ( ExprVar
                                 ( NamedVar "R" ) :| []
                             )
@@ -745,7 +745,7 @@
                         ) Positive
                         ( RelationSymbol
                             ( Command "in" )
-                        )
+                        ) []
                         ( ExprOp
                             [ Just
                                 ( Command "qrefltracl" )
@@ -804,7 +804,7 @@
                         ) Positive
                         ( RelationSymbol
                             ( Command "in" )
-                        )
+                        ) []
                         ( ExprVar
                             ( NamedVar "A" ) :| []
                         )
@@ -830,7 +830,7 @@
                     ) Positive
                     ( RelationSymbol
                         ( Command "in" )
-                    )
+                    ) []
                     ( ExprOp
                         [ Just
                             ( Command "refltracl" )
@@ -871,7 +871,7 @@
                             ) Positive
                             ( RelationSymbol
                                 ( Command "in" )
-                            )
+                            ) []
                             ( ExprOp
                                 [ Just
                                     ( Command "refltracl" )
@@ -909,7 +909,7 @@
                             ) Positive
                             ( RelationSymbol
                                 ( Command "in" )
-                            )
+                            ) []
                             ( ExprVar
                                 ( NamedVar "R" ) :| []
                             )
@@ -935,7 +935,7 @@
                         ) Positive
                         ( RelationSymbol
                             ( Command "in" )
-                        )
+                        ) []
                         ( ExprOp
                             [ Just
                                 ( Command "refltracl" )
@@ -993,7 +993,7 @@
                         ) Positive
                         ( RelationSymbol
                             ( Command "in" )
-                        )
+                        ) []
                         ( ExprOp
                             [ Just
                                 ( Command "fld" )
@@ -1028,7 +1028,7 @@
                         ) Positive
                         ( RelationSymbol
                             ( Command "in" )
-                        )
+                        ) []
                         ( ExprOp
                             [ Just
                                 ( Command "pow" )
@@ -1057,7 +1057,7 @@
                     ) Positive
                     ( RelationSymbol
                         ( Command "in" )
-                    )
+                    ) []
                     ( ExprOp
                         [ Just
                             ( Command "acc" )
diff --git a/test/golden/no-reflexive-set/parsing.golden b/test/golden/no-reflexive-set/parsing.golden
index 3de5dcc..d81dabd 100644
--- a/test/golden/no-reflexive-set/parsing.golden
+++ b/test/golden/no-reflexive-set/parsing.golden
@@ -34,7 +34,7 @@
                         ) Negative
                         ( RelationSymbol
                             ( Command "in" )
-                        )
+                        ) []
                         ( ExprVar
                             ( NamedVar "A" ) :| []
                         )
diff --git a/test/golden/proofassume/parsing.golden b/test/golden/proofassume/parsing.golden
index 57e542c..bf249ed 100644
--- a/test/golden/proofassume/parsing.golden
+++ b/test/golden/proofassume/parsing.golden
@@ -16,7 +16,7 @@
                         ) Positive
                         ( RelationSymbol
                             ( Command "in" )
-                        )
+                        ) []
                         ( ExprVar
                             ( NamedVar "y" ) :| []
                         )
@@ -31,7 +31,7 @@
                         ) Positive
                         ( RelationSymbol
                             ( Command "in" )
-                        )
+                        ) []
                         ( ExprVar
                             ( NamedVar "y" ) :| []
                         )
@@ -56,7 +56,7 @@
                     ) Positive
                     ( RelationSymbol
                         ( Command "in" )
-                    )
+                    ) []
                     ( ExprVar
                         ( NamedVar "y" ) :| []
                     )
@@ -72,7 +72,7 @@
                         ) Positive
                         ( RelationSymbol
                             ( Command "in" )
-                        )
+                        ) []
                         ( ExprVar
                             ( NamedVar "y" ) :| []
                         )
@@ -100,7 +100,7 @@
                             ) Positive
                             ( RelationSymbol
                                 ( Command "in" )
-                            )
+                            ) []
                             ( ExprVar
                                 ( NamedVar "y" ) :| []
                             )
@@ -115,7 +115,7 @@
                             ) Positive
                             ( RelationSymbol
                                 ( Command "in" )
-                            )
+                            ) []
                             ( ExprVar
                                 ( NamedVar "b" ) :| []
                             )
@@ -131,7 +131,7 @@
                         ) Positive
                         ( RelationSymbol
                             ( Command "in" )
-                        )
+                        ) []
                         ( ExprVar
                             ( NamedVar "y" ) :| []
                         )
@@ -156,7 +156,7 @@
                     ) Positive
                     ( RelationSymbol
                         ( Command "in" )
-                    )
+                    ) []
                     ( ExprVar
                         ( NamedVar "b" ) :| []
                     )
@@ -172,7 +172,7 @@
                         ) Positive
                         ( RelationSymbol
                             ( Command "in" )
-                        )
+                        ) []
                         ( ExprVar
                             ( NamedVar "y" ) :| []
                         )
@@ -188,7 +188,7 @@
                             ) Positive
                             ( RelationSymbol
                                 ( Command "in" )
-                            )
+                            ) []
                             ( ExprVar
                                 ( NamedVar "y" ) :| []
                             )
diff --git a/test/golden/proofdefinefunction/parsing.golden b/test/golden/proofdefinefunction/parsing.golden
index eba14ec..c1ba1d0 100644
--- a/test/golden/proofdefinefunction/parsing.golden
+++ b/test/golden/proofdefinefunction/parsing.golden
@@ -72,7 +72,7 @@
                     ) Positive
                     ( RelationSymbol
                         ( Symbol "=" )
-                    )
+                    ) []
                     ( ExprVar
                         ( NamedVar "f" ) :| []
                     )
@@ -113,7 +113,7 @@
                     ) Positive
                     ( RelationSymbol
                         ( Symbol "=" )
-                    )
+                    ) []
                     ( ExprVar
                         ( NamedVar "f" ) :| []
                     )
@@ -139,7 +139,7 @@
                         ) Positive
                         ( RelationSymbol
                             ( Command "in" )
-                        )
+                        ) []
                         ( ExprVar
                             ( NamedVar "y" ) :| []
                         )
@@ -154,7 +154,7 @@
                         ) Positive
                         ( RelationSymbol
                             ( Command "in" )
-                        )
+                        ) []
                         ( ExprVar
                             ( NamedVar "y" ) :| []
                         )
diff --git a/test/golden/prooffix/parsing.golden b/test/golden/prooffix/parsing.golden
index 26b2b35..2702f25 100644
--- a/test/golden/prooffix/parsing.golden
+++ b/test/golden/prooffix/parsing.golden
@@ -17,7 +17,7 @@
                         ) Positive
                         ( RelationSymbol
                             ( Symbol "=" )
-                        )
+                        ) []
                         ( ExprVar
                             ( NamedVar "x" ) :| []
                         )
@@ -44,7 +44,7 @@
                         ) Positive
                         ( RelationSymbol
                             ( Symbol "=" )
-                        )
+                        ) []
                         ( ExprVar
                             ( NamedVar "x" ) :| []
                         )
diff --git a/test/golden/relation-notation/parsing.golden b/test/golden/relation-notation/parsing.golden
index 33f2808..bccafe0 100644
--- a/test/golden/relation-notation/parsing.golden
+++ b/test/golden/relation-notation/parsing.golden
@@ -18,7 +18,7 @@
                             ( ExprVar
                                 ( NamedVar "R" )
                             )
-                        )
+                        ) []
                         ( ExprVar
                             ( NamedVar "y" ) :| []
                         )
@@ -35,7 +35,7 @@
                             ( ExprVar
                                 ( NamedVar "R" )
                             )
-                        )
+                        ) []
                         ( ExprVar
                             ( NamedVar "y" ) :| []
                         )
diff --git a/test/golden/replace/parsing.golden b/test/golden/replace/parsing.golden
index c2cd815..241ca01 100644
--- a/test/golden/replace/parsing.golden
+++ b/test/golden/replace/parsing.golden
@@ -16,7 +16,7 @@
                         ) Positive
                         ( RelationSymbol
                             ( Command "in" )
-                        )
+                        ) []
                         ( ExprOp
                             [ Just
                                 ( Command "cons" )
@@ -45,7 +45,7 @@
                             ) Positive
                             ( RelationSymbol
                                 ( Symbol "=" )
-                            )
+                            ) []
                             ( ExprVar
                                 ( NamedVar "y" ) :| []
                             )
@@ -60,7 +60,7 @@
                             ) Positive
                             ( RelationSymbol
                                 ( Command "in" )
-                            )
+                            ) []
                             ( ExprVar
                                 ( NamedVar "X" ) :| []
                             )
@@ -176,7 +176,7 @@
                     ) Positive
                     ( RelationSymbol
                         ( Command "in" )
-                    )
+                    ) []
                     ( ExprOp
                         [ Nothing
                         , Just
@@ -229,7 +229,7 @@
                         ) Positive
                         ( RelationSymbol
                             ( Symbol "=" )
-                        )
+                        ) []
                         ( ExprFiniteSet
                             ( ExprVar
                                 ( NamedVar "x" ) :| []
@@ -266,7 +266,7 @@
                     ) Positive
                     ( RelationSymbol
                         ( Symbol "=" )
-                    )
+                    ) []
                     ( ExprReplace
                         ( ExprOp
                             [ Just
diff --git a/test/golden/russell/parsing.golden b/test/golden/russell/parsing.golden
index f924229..9f5dc37 100644
--- a/test/golden/russell/parsing.golden
+++ b/test/golden/russell/parsing.golden
@@ -57,7 +57,7 @@
                         ) Positive
                         ( RelationSymbol
                             ( Command "in" )
-                        )
+                        ) []
                         ( ExprVar
                             ( NamedVar "V" ) :| []
                         )
@@ -147,7 +147,7 @@
                                 ) Negative
                                 ( RelationSymbol
                                     ( Command "in" )
-                                )
+                                ) []
                                 ( ExprVar
                                     ( NamedVar "x" ) :| []
                                 )
@@ -165,7 +165,7 @@
                                     ) Positive
                                     ( RelationSymbol
                                         ( Command "in" )
-                                    )
+                                    ) []
                                     ( ExprVar
                                         ( NamedVar "R" ) :| []
                                     )
@@ -180,7 +180,7 @@
                                     ) Negative
                                     ( RelationSymbol
                                         ( Command "in" )
-                                    )
+                                    ) []
                                     ( ExprVar
                                         ( NamedVar "R" ) :| []
                                     )
diff --git a/test/golden/separation/parsing.golden b/test/golden/separation/parsing.golden
index 2a2110f..132f408 100644
--- a/test/golden/separation/parsing.golden
+++ b/test/golden/separation/parsing.golden
@@ -15,7 +15,7 @@
                     ) Positive
                     ( RelationSymbol
                         ( Symbol "=" )
-                    )
+                    ) []
                     ( ExprSep
                         ( NamedVar "x" )
                         ( ExprVar
@@ -29,7 +29,7 @@
                                     ) Positive
                                     ( RelationSymbol
                                         ( Symbol "=" )
-                                    )
+                                    ) []
                                     ( ExprVar
                                         ( NamedVar "x" ) :| []
                                     )
diff --git a/test/golden/union/parsing.golden b/test/golden/union/parsing.golden
index 391f039..3ccdc08 100644
--- a/test/golden/union/parsing.golden
+++ b/test/golden/union/parsing.golden
@@ -19,7 +19,7 @@
                                 ) Positive
                                 ( RelationSymbol
                                     ( Command "in" )
-                                )
+                                ) []
                                 ( ExprVar
                                     ( NamedVar "A" ) :| []
                                 )
@@ -34,7 +34,7 @@
                                 ) Positive
                                 ( RelationSymbol
                                     ( Command "in" )
-                                )
+                                ) []
                                 ( ExprVar
                                     ( NamedVar "B" ) :| []
                                 )
@@ -52,7 +52,7 @@
                     ) Positive
                     ( RelationSymbol
                         ( Symbol "=" )
-                    )
+                    ) []
                     ( ExprVar
                         ( NamedVar "B" ) :| []
                     )
@@ -96,7 +96,7 @@
                         ) Positive
                         ( RelationSymbol
                             ( Command "in" )
-                        )
+                        ) []
                         ( ExprOp
                             [ Nothing
                             , Just
@@ -121,7 +121,7 @@
                             ) Positive
                             ( RelationSymbol
                                 ( Command "in" )
-                            )
+                            ) []
                             ( ExprVar
                                 ( NamedVar "A" ) :| []
                             )
@@ -136,7 +136,7 @@
                             ) Positive
                             ( RelationSymbol
                                 ( Command "in" )
-                            )
+                            ) []
                             ( ExprVar
                                 ( NamedVar "B" ) :| []
                             )
@@ -172,7 +172,7 @@
                     ) Positive
                     ( RelationSymbol
                         ( Symbol "=" )
-                    )
+                    ) []
                     ( ExprOp
                         [ Nothing
                         , Just
@@ -224,7 +224,7 @@
                     ) Positive
                     ( RelationSymbol
                         ( Symbol "=" )
-                    )
+                    ) []
                     ( ExprOp
                         [ Nothing
                         , Just
@@ -269,7 +269,7 @@
                             ) Positive
                             ( RelationSymbol
                                 ( Command "in" )
-                            )
+                            ) []
                             ( ExprOp
                                 [ Nothing
                                 , Just
@@ -302,7 +302,7 @@
                             ) Positive
                             ( RelationSymbol
                                 ( Command "in" )
-                            )
+                            ) []
                             ( ExprOp
                                 [ Nothing
                                 , Just
@@ -341,7 +341,7 @@
                                 ) Positive
                                 ( RelationSymbol
                                     ( Command "in" )
-                                )
+                                ) []
                                 ( ExprOp
                                     [ Nothing
                                     , Just
@@ -374,7 +374,7 @@
                                 ) Positive
                                 ( RelationSymbol
                                     ( Command "in" )
-                                )
+                                ) []
                                 ( ExprOp
                                     [ Nothing
                                     , Just