summaryrefslogtreecommitdiff
path: root/test/golden/indefinite-terms/glossing.golden
diff options
context:
space:
mode:
Diffstat (limited to 'test/golden/indefinite-terms/glossing.golden')
-rw-r--r--test/golden/indefinite-terms/glossing.golden31
1 files changed, 31 insertions, 0 deletions
diff --git a/test/golden/indefinite-terms/glossing.golden b/test/golden/indefinite-terms/glossing.golden
new file mode 100644
index 0000000..b7d3d2a
--- /dev/null
+++ b/test/golden/indefinite-terms/glossing.golden
@@ -0,0 +1,31 @@
+[ BlockLemma
+ ( SourcePos
+ { sourceName = "test/examples/indefinite-terms.tex"
+ , sourceLine = Pos 1
+ , sourceColumn = Pos 1
+ }
+ )
+ ( Marker "indefinite_test_forall" )
+ ( Lemma []
+ ( Quantified Universally
+ ( Scope
+ ( Connected Implication ( PropositionalConstant IsTop ) ( PropositionalConstant IsTop ) )
+ )
+ )
+ )
+, BlockLemma
+ ( SourcePos
+ { sourceName = "test/examples/indefinite-terms.tex"
+ , sourceLine = Pos 5
+ , sourceColumn = Pos 1
+ }
+ )
+ ( Marker "indefinite_test_exists" )
+ ( Lemma []
+ ( Quantified Existentially
+ ( Scope
+ ( Connected Conjunction ( PropositionalConstant IsTop ) ( PropositionalConstant IsTop ) )
+ )
+ )
+ )
+] \ No newline at end of file