summaryrefslogtreecommitdiff
path: root/test/golden/relation-notation/generating tasks.golden
diff options
context:
space:
mode:
Diffstat (limited to 'test/golden/relation-notation/generating tasks.golden')
-rw-r--r--test/golden/relation-notation/generating tasks.golden61
1 files changed, 61 insertions, 0 deletions
diff --git a/test/golden/relation-notation/generating tasks.golden b/test/golden/relation-notation/generating tasks.golden
new file mode 100644
index 0000000..401b93f
--- /dev/null
+++ b/test/golden/relation-notation/generating tasks.golden
@@ -0,0 +1,61 @@
+[ Task
+ { taskDirectness = Direct
+ , taskHypotheses = []
+ , taskConjectureLabel = Marker "mathrel_notation_test"
+ , taskConjecture = Connected Implication
+ ( TermSymbol
+ ( SymbolPredicate
+ ( PredicateRelation
+ ( Command "in" )
+ )
+ )
+ [ TermSymbol
+ ( SymbolMixfix
+ [ Just
+ ( Command "pair" )
+ , Just InvisibleBraceL
+ , Nothing
+ , Just InvisibleBraceR
+ , Just InvisibleBraceL
+ , Nothing
+ , Just InvisibleBraceR
+ ]
+ )
+ [ TermVar
+ ( NamedVar "x" )
+ , TermVar
+ ( NamedVar "y" )
+ ]
+ , TermVar
+ ( NamedVar "R" )
+ ]
+ )
+ ( TermSymbol
+ ( SymbolPredicate
+ ( PredicateRelation
+ ( Command "in" )
+ )
+ )
+ [ TermSymbol
+ ( SymbolMixfix
+ [ Just
+ ( Command "pair" )
+ , Just InvisibleBraceL
+ , Nothing
+ , Just InvisibleBraceR
+ , Just InvisibleBraceL
+ , Nothing
+ , Just InvisibleBraceR
+ ]
+ )
+ [ TermVar
+ ( NamedVar "x" )
+ , TermVar
+ ( NamedVar "y" )
+ ]
+ , TermVar
+ ( NamedVar "R" )
+ ]
+ )
+ }
+] \ No newline at end of file