Sketch noun coord, symbols for reals

15 files changed, 1197 insertions, 25 deletions

diff --git a/test/examples/coord.tex b/test/examples/coord.tex
index 6dc8d5a..9987506 100644
--- a/test/examples/coord.tex
+++ b/test/examples/coord.tex
@@ -35,3 +35,8 @@
 \begin{proposition}\label{adjs}
     $x$ is foo and baz.
 \end{proposition}
+
+\begin{proposition}\label{are_nouns}
+    Let $x, y$ be foo bars.
+    Then $x$ and $y$ are foo bars.
+\end{proposition}
diff --git a/test/examples/formula.tex b/test/examples/formula.tex
index c029402..e3b1e29 100644
--- a/test/examples/formula.tex
+++ b/test/examples/formula.tex
@@ -5,3 +5,7 @@
 \begin{proposition}\label{formula_test_exists}
     $\exists x, y. x = y$.
 \end{proposition}
+
+\begin{proposition}\label{formula_test_not_exists}
+    $\exists x, y. x = y$ if and only if not $\exists x. x \neq x$.
+\end{proposition}
diff --git a/test/examples/signature.tex b/test/examples/signature.tex
deleted file mode 100644
index 4d794a9..0000000
--- a/test/examples/signature.tex
+++ /dev/null
@@ -1,19 +0,0 @@
-\begin{signature}\label{triangle}
-    $x$ can be a number.
-\end{signature}
-
-\begin{signature}\label{even}
-    $x$ can be even.
-\end{signature}
-
-\begin{signature}\label{div}
-    $x$ can divide $y$.
-\end{signature}
-
-\begin{signature}\label{square}
-    The square of $x$ is a number.
-\end{signature}
-
-\begin{signature}\label{nless}
-    $x \nless y$ is a proposition.
-\end{signature}
diff --git a/test/golden/abbr/parsing.golden b/test/golden/abbr/parsing.golden
index bad58c3..2bc8148 100644
--- a/test/golden/abbr/parsing.golden
+++ b/test/golden/abbr/parsing.golden
@@ -126,7 +126,7 @@
             ( TermExpr
                 ( ExprVar
                     ( NamedVar "x" )
-                )
+                ) :| []
             ) NounPhrase ( [] )
             ( Noun
                 ( SgPl
@@ -305,7 +305,7 @@
                 ( TermExpr
                     ( ExprVar
                         ( NamedVar "x" )
-                    )
+                    ) :| []
                 ) NounPhrase ( [] )
                 ( Noun
                     ( SgPl
diff --git a/test/golden/coord/encoding tasks.golden b/test/golden/coord/encoding tasks.golden
index 3776aed..08eb73e 100644
--- a/test/golden/coord/encoding tasks.golden
+++ b/test/golden/coord/encoding tasks.golden
@@ -38,4 +38,16 @@ fof(adj_nouns,axiom,![Xx,Xy]:((bar(Xx)&foo(Xx)&bar(Xy)&foo(Xy))=>Xx=Xx)).
 fof(nouns,axiom,![Xx,Xy]:((bar(Xx)&bar(Xy))=>Xx=Xx)).
 fof(baz,axiom,![Xx]:(baz(Xx)<=>Xx=Xx)).
 fof(foo,axiom,![Xx]:(foo(Xx)<=>Xx=Xx)).
-fof(bar,axiom,![Xx]:(bar(Xx)<=>Xx=Xx)).
\ No newline at end of file
+fof(bar,axiom,![Xx]:(bar(Xx)<=>Xx=Xx)).
+------------------
+fof(are_nouns,conjecture,bar(fx)&foo(fx)&bar(fy)&foo(fy)).
+fof(adjs,axiom,![Xx]:(foo(Xx)&baz(Xx))).
+fof(noun_verb,axiom,![Xx,Xy]:(Xx=Xy<=>(bar(Xx)&Xx=Xy))).
+fof(nouns_suchthat,axiom,![Xx,Xy]:((foo(Xx)&baz(Xy)&bar(Xx)&bar(Xy))=>Xx=Xx)).
+fof(adj_nouns,axiom,![Xx,Xy]:((bar(Xx)&foo(Xx)&bar(Xy)&foo(Xy))=>Xx=Xx)).
+fof(nouns,axiom,![Xx,Xy]:((bar(Xx)&bar(Xy))=>Xx=Xx)).
+fof(baz,axiom,![Xx]:(baz(Xx)<=>Xx=Xx)).
+fof(foo,axiom,![Xx]:(foo(Xx)<=>Xx=Xx)).
+fof(bar,axiom,![Xx]:(bar(Xx)<=>Xx=Xx)).
+fof(are_nouns1,axiom,bar(fy)&foo(fy)).
+fof(are_nouns2,axiom,bar(fx)&foo(fx)).
\ No newline at end of file
diff --git a/test/golden/coord/generating tasks.golden b/test/golden/coord/generating tasks.golden
index 0e43d0e..df07901 100644
--- a/test/golden/coord/generating tasks.golden
+++ b/test/golden/coord/generating tasks.golden
@@ -1965,4 +1965,683 @@
             ]
         )
     }
+, Task
+    { taskDirectness = Direct
+    , taskHypotheses =
+        [
+            ( Marker "adjs"
+            , Quantified Universally
+                ( Scope
+                    ( Connected Conjunction
+                        ( TermSymbol
+                            ( SymbolPredicate
+                                ( PredicateAdj
+                                    [ Just
+                                        ( Word "foo" )
+                                    ]
+                                )
+                            )
+                            [ TermVar
+                                ( B
+                                    ( NamedVar "x" )
+                                )
+                            ]
+                        )
+                        ( TermSymbol
+                            ( SymbolPredicate
+                                ( PredicateAdj
+                                    [ Just
+                                        ( Word "baz" )
+                                    ]
+                                )
+                            )
+                            [ TermVar
+                                ( B
+                                    ( NamedVar "x" )
+                                )
+                            ]
+                        )
+                    )
+                )
+            )
+        ,
+            ( Marker "noun_verb"
+            , Quantified Universally
+                ( Scope
+                    ( Connected Equivalence
+                        ( TermSymbol
+                            ( SymbolPredicate
+                                ( PredicateRelation
+                                    ( Symbol "=" )
+                                )
+                            )
+                            [ TermVar
+                                ( B
+                                    ( NamedVar "x" )
+                                )
+                            , TermVar
+                                ( B
+                                    ( NamedVar "y" )
+                                )
+                            ]
+                        )
+                        ( Connected Conjunction
+                            ( TermSymbol
+                                ( SymbolPredicate
+                                    ( PredicateNoun
+                                        ( SgPl
+                                            { sg =
+                                                [ Just
+                                                    ( Word "bar" )
+                                                ]
+                                            , pl =
+                                                [ Just
+                                                    ( Word "bars" )
+                                                ]
+                                            }
+                                        )
+                                    )
+                                )
+                                [ TermVar
+                                    ( B
+                                        ( NamedVar "x" )
+                                    )
+                                ]
+                            )
+                            ( TermSymbol
+                                ( SymbolPredicate
+                                    ( PredicateRelation
+                                        ( Symbol "=" )
+                                    )
+                                )
+                                [ TermVar
+                                    ( B
+                                        ( NamedVar "x" )
+                                    )
+                                , TermVar
+                                    ( B
+                                        ( NamedVar "y" )
+                                    )
+                                ]
+                            )
+                        )
+                    )
+                )
+            )
+        ,
+            ( Marker "nouns_suchthat"
+            , Quantified Universally
+                ( Scope
+                    ( Connected Implication
+                        ( Connected Conjunction
+                            ( Connected Conjunction
+                                ( Connected Conjunction
+                                    ( TermSymbol
+                                        ( SymbolPredicate
+                                            ( PredicateAdj
+                                                [ Just
+                                                    ( Word "foo" )
+                                                ]
+                                            )
+                                        )
+                                        [ TermVar
+                                            ( B
+                                                ( NamedVar "x" )
+                                            )
+                                        ]
+                                    )
+                                    ( TermSymbol
+                                        ( SymbolPredicate
+                                            ( PredicateAdj
+                                                [ Just
+                                                    ( Word "baz" )
+                                                ]
+                                            )
+                                        )
+                                        [ TermVar
+                                            ( B
+                                                ( NamedVar "y" )
+                                            )
+                                        ]
+                                    )
+                                )
+                                ( TermSymbol
+                                    ( SymbolPredicate
+                                        ( PredicateNoun
+                                            ( SgPl
+                                                { sg =
+                                                    [ Just
+                                                        ( Word "bar" )
+                                                    ]
+                                                , pl =
+                                                    [ Just
+                                                        ( Word "bars" )
+                                                    ]
+                                                }
+                                            )
+                                        )
+                                    )
+                                    [ TermVar
+                                        ( B
+                                            ( NamedVar "x" )
+                                        )
+                                    ]
+                                )
+                            )
+                            ( TermSymbol
+                                ( SymbolPredicate
+                                    ( PredicateNoun
+                                        ( SgPl
+                                            { sg =
+                                                [ Just
+                                                    ( Word "bar" )
+                                                ]
+                                            , pl =
+                                                [ Just
+                                                    ( Word "bars" )
+                                                ]
+                                            }
+                                        )
+                                    )
+                                )
+                                [ TermVar
+                                    ( B
+                                        ( NamedVar "y" )
+                                    )
+                                ]
+                            )
+                        )
+                        ( TermSymbol
+                            ( SymbolPredicate
+                                ( PredicateRelation
+                                    ( Symbol "=" )
+                                )
+                            )
+                            [ TermVar
+                                ( B
+                                    ( NamedVar "x" )
+                                )
+                            , TermVar
+                                ( B
+                                    ( NamedVar "x" )
+                                )
+                            ]
+                        )
+                    )
+                )
+            )
+        ,
+            ( Marker "adj_nouns"
+            , Quantified Universally
+                ( Scope
+                    ( Connected Implication
+                        ( Connected Conjunction
+                            ( Connected Conjunction
+                                ( TermSymbol
+                                    ( SymbolPredicate
+                                        ( PredicateNoun
+                                            ( SgPl
+                                                { sg =
+                                                    [ Just
+                                                        ( Word "bar" )
+                                                    ]
+                                                , pl =
+                                                    [ Just
+                                                        ( Word "bars" )
+                                                    ]
+                                                }
+                                            )
+                                        )
+                                    )
+                                    [ TermVar
+                                        ( B
+                                            ( NamedVar "x" )
+                                        )
+                                    ]
+                                )
+                                ( TermSymbol
+                                    ( SymbolPredicate
+                                        ( PredicateAdj
+                                            [ Just
+                                                ( Word "foo" )
+                                            ]
+                                        )
+                                    )
+                                    [ TermVar
+                                        ( B
+                                            ( NamedVar "x" )
+                                        )
+                                    ]
+                                )
+                            )
+                            ( Connected Conjunction
+                                ( TermSymbol
+                                    ( SymbolPredicate
+                                        ( PredicateNoun
+                                            ( SgPl
+                                                { sg =
+                                                    [ Just
+                                                        ( Word "bar" )
+                                                    ]
+                                                , pl =
+                                                    [ Just
+                                                        ( Word "bars" )
+                                                    ]
+                                                }
+                                            )
+                                        )
+                                    )
+                                    [ TermVar
+                                        ( B
+                                            ( NamedVar "y" )
+                                        )
+                                    ]
+                                )
+                                ( TermSymbol
+                                    ( SymbolPredicate
+                                        ( PredicateAdj
+                                            [ Just
+                                                ( Word "foo" )
+                                            ]
+                                        )
+                                    )
+                                    [ TermVar
+                                        ( B
+                                            ( NamedVar "y" )
+                                        )
+                                    ]
+                                )
+                            )
+                        )
+                        ( TermSymbol
+                            ( SymbolPredicate
+                                ( PredicateRelation
+                                    ( Symbol "=" )
+                                )
+                            )
+                            [ TermVar
+                                ( B
+                                    ( NamedVar "x" )
+                                )
+                            , TermVar
+                                ( B
+                                    ( NamedVar "x" )
+                                )
+                            ]
+                        )
+                    )
+                )
+            )
+        ,
+            ( Marker "nouns"
+            , Quantified Universally
+                ( Scope
+                    ( Connected Implication
+                        ( Connected Conjunction
+                            ( TermSymbol
+                                ( SymbolPredicate
+                                    ( PredicateNoun
+                                        ( SgPl
+                                            { sg =
+                                                [ Just
+                                                    ( Word "bar" )
+                                                ]
+                                            , pl =
+                                                [ Just
+                                                    ( Word "bars" )
+                                                ]
+                                            }
+                                        )
+                                    )
+                                )
+                                [ TermVar
+                                    ( B
+                                        ( NamedVar "x" )
+                                    )
+                                ]
+                            )
+                            ( TermSymbol
+                                ( SymbolPredicate
+                                    ( PredicateNoun
+                                        ( SgPl
+                                            { sg =
+                                                [ Just
+                                                    ( Word "bar" )
+                                                ]
+                                            , pl =
+                                                [ Just
+                                                    ( Word "bars" )
+                                                ]
+                                            }
+                                        )
+                                    )
+                                )
+                                [ TermVar
+                                    ( B
+                                        ( NamedVar "y" )
+                                    )
+                                ]
+                            )
+                        )
+                        ( TermSymbol
+                            ( SymbolPredicate
+                                ( PredicateRelation
+                                    ( Symbol "=" )
+                                )
+                            )
+                            [ TermVar
+                                ( B
+                                    ( NamedVar "x" )
+                                )
+                            , TermVar
+                                ( B
+                                    ( NamedVar "x" )
+                                )
+                            ]
+                        )
+                    )
+                )
+            )
+        ,
+            ( Marker "baz"
+            , Quantified Universally
+                ( Scope
+                    ( Connected Equivalence
+                        ( TermSymbol
+                            ( SymbolPredicate
+                                ( PredicateAdj
+                                    [ Just
+                                        ( Word "baz" )
+                                    ]
+                                )
+                            )
+                            [ TermVar
+                                ( B
+                                    ( NamedVar "x" )
+                                )
+                            ]
+                        )
+                        ( Quantified Universally
+                            ( Scope
+                                ( TermSymbol
+                                    ( SymbolPredicate
+                                        ( PredicateRelation
+                                            ( Symbol "=" )
+                                        )
+                                    )
+                                    [ TermVar
+                                        ( F
+                                            ( TermVar
+                                                ( B
+                                                    ( NamedVar "x" )
+                                                )
+                                            )
+                                        )
+                                    , TermVar
+                                        ( F
+                                            ( TermVar
+                                                ( B
+                                                    ( NamedVar "x" )
+                                                )
+                                            )
+                                        )
+                                    ]
+                                )
+                            )
+                        )
+                    )
+                )
+            )
+        ,
+            ( Marker "foo"
+            , Quantified Universally
+                ( Scope
+                    ( Connected Equivalence
+                        ( TermSymbol
+                            ( SymbolPredicate
+                                ( PredicateAdj
+                                    [ Just
+                                        ( Word "foo" )
+                                    ]
+                                )
+                            )
+                            [ TermVar
+                                ( B
+                                    ( NamedVar "x" )
+                                )
+                            ]
+                        )
+                        ( Quantified Universally
+                            ( Scope
+                                ( TermSymbol
+                                    ( SymbolPredicate
+                                        ( PredicateRelation
+                                            ( Symbol "=" )
+                                        )
+                                    )
+                                    [ TermVar
+                                        ( F
+                                            ( TermVar
+                                                ( B
+                                                    ( NamedVar "x" )
+                                                )
+                                            )
+                                        )
+                                    , TermVar
+                                        ( F
+                                            ( TermVar
+                                                ( B
+                                                    ( NamedVar "x" )
+                                                )
+                                            )
+                                        )
+                                    ]
+                                )
+                            )
+                        )
+                    )
+                )
+            )
+        ,
+            ( Marker "bar"
+            , Quantified Universally
+                ( Scope
+                    ( Connected Equivalence
+                        ( TermSymbol
+                            ( SymbolPredicate
+                                ( PredicateNoun
+                                    ( SgPl
+                                        { sg =
+                                            [ Just
+                                                ( Word "bar" )
+                                            ]
+                                        , pl =
+                                            [ Just
+                                                ( Word "bars" )
+                                            ]
+                                        }
+                                    )
+                                )
+                            )
+                            [ TermVar
+                                ( B
+                                    ( NamedVar "x" )
+                                )
+                            ]
+                        )
+                        ( Quantified Universally
+                            ( Scope
+                                ( TermSymbol
+                                    ( SymbolPredicate
+                                        ( PredicateRelation
+                                            ( Symbol "=" )
+                                        )
+                                    )
+                                    [ TermVar
+                                        ( F
+                                            ( TermVar
+                                                ( B
+                                                    ( NamedVar "x" )
+                                                )
+                                            )
+                                        )
+                                    , TermVar
+                                        ( F
+                                            ( TermVar
+                                                ( B
+                                                    ( NamedVar "x" )
+                                                )
+                                            )
+                                        )
+                                    ]
+                                )
+                            )
+                        )
+                    )
+                )
+            )
+        ,
+            ( Marker "are_nouns1"
+            , Connected Conjunction
+                ( TermSymbol
+                    ( SymbolPredicate
+                        ( PredicateNoun
+                            ( SgPl
+                                { sg =
+                                    [ Just
+                                        ( Word "bar" )
+                                    ]
+                                , pl =
+                                    [ Just
+                                        ( Word "bars" )
+                                    ]
+                                }
+                            )
+                        )
+                    )
+                    [ TermVar
+                        ( NamedVar "y" )
+                    ]
+                )
+                ( TermSymbol
+                    ( SymbolPredicate
+                        ( PredicateAdj
+                            [ Just
+                                ( Word "foo" )
+                            ]
+                        )
+                    )
+                    [ TermVar
+                        ( NamedVar "y" )
+                    ]
+                )
+            )
+        ,
+            ( Marker "are_nouns2"
+            , Connected Conjunction
+                ( TermSymbol
+                    ( SymbolPredicate
+                        ( PredicateNoun
+                            ( SgPl
+                                { sg =
+                                    [ Just
+                                        ( Word "bar" )
+                                    ]
+                                , pl =
+                                    [ Just
+                                        ( Word "bars" )
+                                    ]
+                                }
+                            )
+                        )
+                    )
+                    [ TermVar
+                        ( NamedVar "x" )
+                    ]
+                )
+                ( TermSymbol
+                    ( SymbolPredicate
+                        ( PredicateAdj
+                            [ Just
+                                ( Word "foo" )
+                            ]
+                        )
+                    )
+                    [ TermVar
+                        ( NamedVar "x" )
+                    ]
+                )
+            )
+        ]
+    , taskConjectureLabel = Marker "are_nouns"
+    , taskConjecture = Connected Conjunction
+        ( Connected Conjunction
+            ( TermSymbol
+                ( SymbolPredicate
+                    ( PredicateNoun
+                        ( SgPl
+                            { sg =
+                                [ Just
+                                    ( Word "bar" )
+                                ]
+                            , pl =
+                                [ Just
+                                    ( Word "bars" )
+                                ]
+                            }
+                        )
+                    )
+                )
+                [ TermVar
+                    ( NamedVar "x" )
+                ]
+            )
+            ( TermSymbol
+                ( SymbolPredicate
+                    ( PredicateAdj
+                        [ Just
+                            ( Word "foo" )
+                        ]
+                    )
+                )
+                [ TermVar
+                    ( NamedVar "x" )
+                ]
+            )
+        )
+        ( Connected Conjunction
+            ( TermSymbol
+                ( SymbolPredicate
+                    ( PredicateNoun
+                        ( SgPl
+                            { sg =
+                                [ Just
+                                    ( Word "bar" )
+                                ]
+                            , pl =
+                                [ Just
+                                    ( Word "bars" )
+                                ]
+                            }
+                        )
+                    )
+                )
+                [ TermVar
+                    ( NamedVar "y" )
+                ]
+            )
+            ( TermSymbol
+                ( SymbolPredicate
+                    ( PredicateAdj
+                        [ Just
+                            ( Word "foo" )
+                        ]
+                    )
+                )
+                [ TermVar
+                    ( NamedVar "y" )
+                ]
+            )
+        )
+    }
 ]
\ No newline at end of file
diff --git a/test/golden/coord/glossing.golden b/test/golden/coord/glossing.golden
index c051fe9..0ae9b95 100644
--- a/test/golden/coord/glossing.golden
+++ b/test/golden/coord/glossing.golden
@@ -434,4 +434,155 @@
             )
         )
     )
+, BlockLemma
+    ( SourcePos
+        { sourceName = "test/examples/coord.tex"
+        , sourceLine = Pos 39
+        , sourceColumn = Pos 1
+        }
+    )
+    ( Marker "are_nouns" )
+    ( Lemma
+        [ Asm
+            ( Connected Conjunction
+                ( TermSymbol
+                    ( SymbolPredicate
+                        ( PredicateNoun
+                            ( SgPl
+                                { sg =
+                                    [ Just
+                                        ( Word "bar" )
+                                    ]
+                                , pl =
+                                    [ Just
+                                        ( Word "bars" )
+                                    ]
+                                }
+                            )
+                        )
+                    )
+                    [ TermVar
+                        ( NamedVar "x" )
+                    ]
+                )
+                ( TermSymbol
+                    ( SymbolPredicate
+                        ( PredicateAdj
+                            [ Just
+                                ( Word "foo" )
+                            ]
+                        )
+                    )
+                    [ TermVar
+                        ( NamedVar "x" )
+                    ]
+                )
+            )
+        , Asm
+            ( Connected Conjunction
+                ( TermSymbol
+                    ( SymbolPredicate
+                        ( PredicateNoun
+                            ( SgPl
+                                { sg =
+                                    [ Just
+                                        ( Word "bar" )
+                                    ]
+                                , pl =
+                                    [ Just
+                                        ( Word "bars" )
+                                    ]
+                                }
+                            )
+                        )
+                    )
+                    [ TermVar
+                        ( NamedVar "y" )
+                    ]
+                )
+                ( TermSymbol
+                    ( SymbolPredicate
+                        ( PredicateAdj
+                            [ Just
+                                ( Word "foo" )
+                            ]
+                        )
+                    )
+                    [ TermVar
+                        ( NamedVar "y" )
+                    ]
+                )
+            )
+        ]
+        ( Connected Conjunction
+            ( Connected Conjunction
+                ( TermSymbol
+                    ( SymbolPredicate
+                        ( PredicateNoun
+                            ( SgPl
+                                { sg =
+                                    [ Just
+                                        ( Word "bar" )
+                                    ]
+                                , pl =
+                                    [ Just
+                                        ( Word "bars" )
+                                    ]
+                                }
+                            )
+                        )
+                    )
+                    [ TermVar
+                        ( NamedVar "x" )
+                    ]
+                )
+                ( TermSymbol
+                    ( SymbolPredicate
+                        ( PredicateAdj
+                            [ Just
+                                ( Word "foo" )
+                            ]
+                        )
+                    )
+                    [ TermVar
+                        ( NamedVar "x" )
+                    ]
+                )
+            )
+            ( Connected Conjunction
+                ( TermSymbol
+                    ( SymbolPredicate
+                        ( PredicateNoun
+                            ( SgPl
+                                { sg =
+                                    [ Just
+                                        ( Word "bar" )
+                                    ]
+                                , pl =
+                                    [ Just
+                                        ( Word "bars" )
+                                    ]
+                                }
+                            )
+                        )
+                    )
+                    [ TermVar
+                        ( NamedVar "y" )
+                    ]
+                )
+                ( TermSymbol
+                    ( SymbolPredicate
+                        ( PredicateAdj
+                            [ Just
+                                ( Word "foo" )
+                            ]
+                        )
+                    )
+                    [ TermVar
+                        ( NamedVar "y" )
+                    ]
+                )
+            )
+        )
+    )
 ]
\ No newline at end of file
diff --git a/test/golden/coord/parsing.golden b/test/golden/coord/parsing.golden
index 555b86b..65fa82f 100644
--- a/test/golden/coord/parsing.golden
+++ b/test/golden/coord/parsing.golden
@@ -302,7 +302,7 @@
                 ( TermExpr
                     ( ExprVar
                         ( NamedVar "x" )
-                    )
+                    ) :| []
                 ) NounPhrase ( [] )
                 ( Noun
                     ( SgPl
@@ -364,4 +364,71 @@
             )
         )
     )
+, BlockLemma
+    ( SourcePos
+        { sourceName = "test/examples/coord.tex"
+        , sourceLine = Pos 39
+        , sourceColumn = Pos 1
+        }
+    )
+    ( Marker "are_nouns" )
+    ( Lemma
+        [ AsmLetNoun
+            ( NamedVar "x" :|
+                [ NamedVar "y" ]
+            ) NounPhrase
+            (
+                [ AdjL
+                    [ Just
+                        ( Word "foo" )
+                    ] []
+                ]
+            )
+            ( Noun
+                ( SgPl
+                    { sg =
+                        [ Just
+                            ( Word "bar" )
+                        ]
+                    , pl =
+                        [ Just
+                            ( Word "bars" )
+                        ]
+                    }
+                ) []
+            ) ( Nothing ) ( [] ) ( Nothing )
+        ]
+        ( StmtNoun
+            ( TermExpr
+                ( ExprVar
+                    ( NamedVar "x" )
+                ) :|
+                [ TermExpr
+                    ( ExprVar
+                        ( NamedVar "y" )
+                    )
+                ]
+            ) NounPhrase
+            (
+                [ AdjL
+                    [ Just
+                        ( Word "foo" )
+                    ] []
+                ]
+            )
+            ( Noun
+                ( SgPl
+                    { sg =
+                        [ Just
+                            ( Word "bar" )
+                        ]
+                    , pl =
+                        [ Just
+                            ( Word "bars" )
+                        ]
+                    }
+                ) []
+            ) ( Nothing ) ( [] ) ( Nothing )
+        )
+    )
 ]
\ No newline at end of file
diff --git a/test/golden/coord/tokenizing.golden b/test/golden/coord/tokenizing.golden
index 0516d7a..b993832 100644
--- a/test/golden/coord/tokenizing.golden
+++ b/test/golden/coord/tokenizing.golden
@@ -147,4 +147,29 @@
 , Word "baz"
 , Symbol "."
 , EndEnv "proposition"
+, BeginEnv "proposition"
+, Label "are_nouns"
+, Word "let"
+, BeginEnv "math"
+, Variable "x"
+, Symbol ","
+, Variable "y"
+, EndEnv "math"
+, Word "be"
+, Word "foo"
+, Word "bars"
+, Symbol "."
+, Word "then"
+, BeginEnv "math"
+, Variable "x"
+, EndEnv "math"
+, Word "and"
+, BeginEnv "math"
+, Variable "y"
+, EndEnv "math"
+, Word "are"
+, Word "foo"
+, Word "bars"
+, Symbol "."
+, EndEnv "proposition"
 ]
\ No newline at end of file
diff --git a/test/golden/formula/encoding tasks.golden b/test/golden/formula/encoding tasks.golden
index ab149dd..64f4883 100644
--- a/test/golden/formula/encoding tasks.golden
+++ b/test/golden/formula/encoding tasks.golden
@@ -1,4 +1,8 @@
 fof(formula_test_forall,conjecture,![Xx,Xy]:(Xx=Xx&Xy=Xy)).
 ------------------
 fof(formula_test_exists,conjecture,?[Xx,Xy]:Xx=Xy).
+fof(formula_test_forall,axiom,![Xx,Xy]:(Xx=Xx&Xy=Xy)).
+------------------
+fof(formula_test_not_exists,conjecture,?[Xx,Xy]:Xx=Xy<=>~?[Xx]:Xx!=Xx).
+fof(formula_test_exists,axiom,?[Xx,Xy]:Xx=Xy).
 fof(formula_test_forall,axiom,![Xx,Xy]:(Xx=Xx&Xy=Xy)).
\ No newline at end of file
diff --git a/test/golden/formula/generating tasks.golden b/test/golden/formula/generating tasks.golden
index db5d39e..04b4a7d 100644
--- a/test/golden/formula/generating tasks.golden
+++ b/test/golden/formula/generating tasks.golden
@@ -105,4 +105,115 @@
             )
         )
     }
+, Task
+    { taskDirectness = Direct
+    , taskHypotheses =
+        [
+            ( Marker "formula_test_exists"
+            , Quantified Existentially
+                ( Scope
+                    ( TermSymbol
+                        ( SymbolPredicate
+                            ( PredicateRelation
+                                ( Symbol "=" )
+                            )
+                        )
+                        [ TermVar
+                            ( B
+                                ( NamedVar "x" )
+                            )
+                        , TermVar
+                            ( B
+                                ( NamedVar "y" )
+                            )
+                        ]
+                    )
+                )
+            )
+        ,
+            ( Marker "formula_test_forall"
+            , Quantified Universally
+                ( Scope
+                    ( Connected Conjunction
+                        ( TermSymbol
+                            ( SymbolPredicate
+                                ( PredicateRelation
+                                    ( Symbol "=" )
+                                )
+                            )
+                            [ TermVar
+                                ( B
+                                    ( NamedVar "x" )
+                                )
+                            , TermVar
+                                ( B
+                                    ( NamedVar "x" )
+                                )
+                            ]
+                        )
+                        ( TermSymbol
+                            ( SymbolPredicate
+                                ( PredicateRelation
+                                    ( Symbol "=" )
+                                )
+                            )
+                            [ TermVar
+                                ( B
+                                    ( NamedVar "y" )
+                                )
+                            , TermVar
+                                ( B
+                                    ( NamedVar "y" )
+                                )
+                            ]
+                        )
+                    )
+                )
+            )
+        ]
+    , taskConjectureLabel = Marker "formula_test_not_exists"
+    , taskConjecture = Connected Equivalence
+        ( Quantified Existentially
+            ( Scope
+                ( TermSymbol
+                    ( SymbolPredicate
+                        ( PredicateRelation
+                            ( Symbol "=" )
+                        )
+                    )
+                    [ TermVar
+                        ( B
+                            ( NamedVar "x" )
+                        )
+                    , TermVar
+                        ( B
+                            ( NamedVar "y" )
+                        )
+                    ]
+                )
+            )
+        )
+        ( Not
+            ( Quantified Existentially
+                ( Scope
+                    ( TermSymbol
+                        ( SymbolPredicate
+                            ( PredicateRelation
+                                ( Command "neq" )
+                            )
+                        )
+                        [ TermVar
+                            ( B
+                                ( NamedVar "x" )
+                            )
+                        , TermVar
+                            ( B
+                                ( NamedVar "x" )
+                            )
+                        ]
+                    )
+                )
+            )
+        )
+    }
 ]
\ No newline at end of file
diff --git a/test/golden/formula/glossing.golden b/test/golden/formula/glossing.golden
index bb72370..f282b2e 100644
--- a/test/golden/formula/glossing.golden
+++ b/test/golden/formula/glossing.golden
@@ -76,4 +76,58 @@
             )
         )
     )
+, BlockLemma
+    ( SourcePos
+        { sourceName = "test/examples/formula.tex"
+        , sourceLine = Pos 9
+        , sourceColumn = Pos 1
+        }
+    )
+    ( Marker "formula_test_not_exists" )
+    ( Lemma []
+        ( Connected Equivalence
+            ( Quantified Existentially
+                ( Scope
+                    ( TermSymbol
+                        ( SymbolPredicate
+                            ( PredicateRelation
+                                ( Symbol "=" )
+                            )
+                        )
+                        [ TermVar
+                            ( B
+                                ( NamedVar "x" )
+                            )
+                        , TermVar
+                            ( B
+                                ( NamedVar "y" )
+                            )
+                        ]
+                    )
+                )
+            )
+            ( Not
+                ( Quantified Existentially
+                    ( Scope
+                        ( TermSymbol
+                            ( SymbolPredicate
+                                ( PredicateRelation
+                                    ( Command "neq" )
+                                )
+                            )
+                            [ TermVar
+                                ( B
+                                    ( NamedVar "x" )
+                                )
+                            , TermVar
+                                ( B
+                                    ( NamedVar "x" )
+                                )
+                            ]
+                        )
+                    )
+                )
+            )
+        )
+    )
 ]
\ No newline at end of file
diff --git a/test/golden/formula/parsing.golden b/test/golden/formula/parsing.golden
index 4c6321d..7de1fb7 100644
--- a/test/golden/formula/parsing.golden
+++ b/test/golden/formula/parsing.golden
@@ -73,4 +73,56 @@
             )
         )
     )
+, BlockLemma
+    ( SourcePos
+        { sourceName = "test/examples/formula.tex"
+        , sourceLine = Pos 9
+        , sourceColumn = Pos 1
+        }
+    )
+    ( Marker "formula_test_not_exists" )
+    ( Lemma []
+        ( StmtConnected Equivalence
+            ( StmtFormula
+                ( FormulaQuantified Existentially
+                    ( NamedVar "x" :|
+                        [ NamedVar "y" ]
+                    ) Unbounded
+                    ( FormulaChain
+                        ( ChainBase
+                            ( ExprVar
+                                ( NamedVar "x" ) :| []
+                            ) Positive
+                            ( RelationSymbol
+                                ( Symbol "=" )
+                            )
+                            ( ExprVar
+                                ( NamedVar "y" ) :| []
+                            )
+                        )
+                    )
+                )
+            )
+            ( StmtNeg
+                ( StmtFormula
+                    ( FormulaQuantified Existentially
+                        ( NamedVar "x" :| [] ) Unbounded
+                        ( FormulaChain
+                            ( ChainBase
+                                ( ExprVar
+                                    ( NamedVar "x" ) :| []
+                                ) Positive
+                                ( RelationSymbol
+                                    ( Command "neq" )
+                                )
+                                ( ExprVar
+                                    ( NamedVar "x" ) :| []
+                                )
+                            )
+                        )
+                    )
+                )
+            )
+        )
+    )
 ]
\ No newline at end of file
diff --git a/test/golden/formula/tokenizing.golden b/test/golden/formula/tokenizing.golden
index 3cb9b0e..1abe20a 100644
--- a/test/golden/formula/tokenizing.golden
+++ b/test/golden/formula/tokenizing.golden
@@ -30,4 +30,31 @@
 , EndEnv "math"
 , Symbol "."
 , EndEnv "proposition"
+, BeginEnv "proposition"
+, Label "formula_test_not_exists"
+, BeginEnv "math"
+, Command "exists"
+, Variable "x"
+, Symbol ","
+, Variable "y"
+, Symbol "."
+, Variable "x"
+, Symbol "="
+, Variable "y"
+, EndEnv "math"
+, Word "if"
+, Word "and"
+, Word "only"
+, Word "if"
+, Word "not"
+, BeginEnv "math"
+, Command "exists"
+, Variable "x"
+, Symbol "."
+, Variable "x"
+, Command "neq"
+, Variable "x"
+, EndEnv "math"
+, Symbol "."
+, EndEnv "proposition"
 ]
\ No newline at end of file
diff --git a/test/golden/indefinite-terms/parsing.golden b/test/golden/indefinite-terms/parsing.golden
index 8c468ab..2beb5ca 100644
--- a/test/golden/indefinite-terms/parsing.golden
+++ b/test/golden/indefinite-terms/parsing.golden
@@ -21,7 +21,7 @@
                             ]
                         }
                     ) []
-                ) ( Nothing ) ( [] ) ( Nothing )
+                ) ( Nothing ) ( [] ) ( Nothing ) :| []
             ) NounPhrase ( [] )
             ( Noun
                 ( SgPl
@@ -61,7 +61,7 @@
                             ]
                         }
                     ) []
-                ) ( Nothing ) ( [] ) ( Nothing )
+                ) ( Nothing ) ( [] ) ( Nothing ) :| []
             ) NounPhrase ( [] )
             ( Noun
                 ( SgPl