diff options
Diffstat (limited to 'test/golden/formula/generating tasks.golden')
| -rw-r--r-- | test/golden/formula/generating tasks.golden | 331 |
1 files changed, 0 insertions, 331 deletions
diff --git a/test/golden/formula/generating tasks.golden b/test/golden/formula/generating tasks.golden deleted file mode 100644 index 54c2012..0000000 --- a/test/golden/formula/generating tasks.golden +++ /dev/null @@ -1,331 +0,0 @@ -[ Task - { taskDirectness = Direct - , taskHypotheses = [] - , taskConjectureLabel = Marker "formula_test_forall" - , taskLocation = Location - { locFile = "test/examples/formula.tex" - , locLine = 1 - , locColumn = 1 - } - , taskConjecture = Quantified Universally - ( Scope - ( Connected Conjunction - ( TermSymbol - ( Location - { locFile = "test/examples/formula.tex" - , locLine = 2 - , locColumn = 22 - } - ) - ( SymbolPredicate - ( PredicateRelation - ( RelationSymbol - ( Symbol "=" ) - ( ParameterArity 0 ) - ( Marker "eq" ) - ) - ) - ) - [ TermVar - ( B - ( NamedVar "x" ) - ) - , TermVar - ( B - ( NamedVar "x" ) - ) - ] - ) - ( TermSymbol - ( Location - { locFile = "test/examples/formula.tex" - , locLine = 2 - , locColumn = 33 - } - ) - ( SymbolPredicate - ( PredicateRelation - ( RelationSymbol - ( Symbol "=" ) - ( ParameterArity 0 ) - ( Marker "eq" ) - ) - ) - ) - [ TermVar - ( B - ( NamedVar "y" ) - ) - , TermVar - ( B - ( NamedVar "y" ) - ) - ] - ) - ) - ) - } -, Task - { taskDirectness = Direct - , taskHypotheses = - [ Hypothesis Marker "formula_test_forall" Quantified Universally - ( Scope - ( Connected Conjunction - ( TermSymbol - ( Location - { locFile = "test/examples/formula.tex" - , locLine = 2 - , locColumn = 22 - } - ) - ( SymbolPredicate - ( PredicateRelation - ( RelationSymbol - ( Symbol "=" ) - ( ParameterArity 0 ) - ( Marker "eq" ) - ) - ) - ) - [ TermVar - ( B - ( NamedVar "x" ) - ) - , TermVar - ( B - ( NamedVar "x" ) - ) - ] - ) - ( TermSymbol - ( Location - { locFile = "test/examples/formula.tex" - , locLine = 2 - , locColumn = 33 - } - ) - ( SymbolPredicate - ( PredicateRelation - ( RelationSymbol - ( Symbol "=" ) - ( ParameterArity 0 ) - ( Marker "eq" ) - ) - ) - ) - [ TermVar - ( B - ( NamedVar "y" ) - ) - , TermVar - ( B - ( NamedVar "y" ) - ) - ] - ) - ) - ) - ] - , taskConjectureLabel = Marker "formula_test_exists" - , taskLocation = Location - { locFile = "test/examples/formula.tex" - , locLine = 5 - , locColumn = 1 - } - , taskConjecture = Quantified Existentially - ( Scope - ( TermSymbol - ( Location - { locFile = "test/examples/formula.tex" - , locLine = 6 - , locColumn = 22 - } - ) - ( SymbolPredicate - ( PredicateRelation - ( RelationSymbol - ( Symbol "=" ) - ( ParameterArity 0 ) - ( Marker "eq" ) - ) - ) - ) - [ TermVar - ( B - ( NamedVar "x" ) - ) - , TermVar - ( B - ( NamedVar "y" ) - ) - ] - ) - ) - } -, Task - { taskDirectness = Direct - , taskHypotheses = - [ Hypothesis Marker "formula_test_exists" Quantified Existentially - ( Scope - ( TermSymbol - ( Location - { locFile = "test/examples/formula.tex" - , locLine = 6 - , locColumn = 22 - } - ) - ( SymbolPredicate - ( PredicateRelation - ( RelationSymbol - ( Symbol "=" ) - ( ParameterArity 0 ) - ( Marker "eq" ) - ) - ) - ) - [ TermVar - ( B - ( NamedVar "x" ) - ) - , TermVar - ( B - ( NamedVar "y" ) - ) - ] - ) - ) - , Hypothesis Marker "formula_test_forall" Quantified Universally - ( Scope - ( Connected Conjunction - ( TermSymbol - ( Location - { locFile = "test/examples/formula.tex" - , locLine = 2 - , locColumn = 22 - } - ) - ( SymbolPredicate - ( PredicateRelation - ( RelationSymbol - ( Symbol "=" ) - ( ParameterArity 0 ) - ( Marker "eq" ) - ) - ) - ) - [ TermVar - ( B - ( NamedVar "x" ) - ) - , TermVar - ( B - ( NamedVar "x" ) - ) - ] - ) - ( TermSymbol - ( Location - { locFile = "test/examples/formula.tex" - , locLine = 2 - , locColumn = 33 - } - ) - ( SymbolPredicate - ( PredicateRelation - ( RelationSymbol - ( Symbol "=" ) - ( ParameterArity 0 ) - ( Marker "eq" ) - ) - ) - ) - [ TermVar - ( B - ( NamedVar "y" ) - ) - , TermVar - ( B - ( NamedVar "y" ) - ) - ] - ) - ) - ) - ] - , taskConjectureLabel = Marker "formula_test_not_exists" - , taskLocation = Location - { locFile = "test/examples/formula.tex" - , locLine = 9 - , locColumn = 1 - } - , taskConjecture = Connected Equivalence - ( Quantified Existentially - ( Scope - ( TermSymbol - ( Location - { locFile = "test/examples/formula.tex" - , locLine = 10 - , locColumn = 22 - } - ) - ( SymbolPredicate - ( PredicateRelation - ( RelationSymbol - ( Symbol "=" ) - ( ParameterArity 0 ) - ( Marker "eq" ) - ) - ) - ) - [ TermVar - ( B - ( NamedVar "x" ) - ) - , TermVar - ( B - ( NamedVar "y" ) - ) - ] - ) - ) - ) - ( Not - ( Location - { locFile = "test/examples/formula.tex" - , locLine = 10 - , locColumn = 42 - } - ) - ( Quantified Existentially - ( Scope - ( TermSymbol - ( Location - { locFile = "test/examples/formula.tex" - , locLine = 10 - , locColumn = 60 - } - ) - ( SymbolPredicate - ( PredicateRelation - ( RelationSymbol - ( Command "neq" ) - ( ParameterArity 0 ) - ( Marker "neq" ) - ) - ) - ) - [ TermVar - ( B - ( NamedVar "x" ) - ) - , TermVar - ( B - ( NamedVar "x" ) - ) - ] - ) - ) - ) - ) - } -]
\ No newline at end of file |