diff options
Diffstat (limited to 'test/golden/relation-notation')
| -rw-r--r-- | test/golden/relation-notation/encoding tasks.golden | 1 | ||||
| -rw-r--r-- | test/golden/relation-notation/generating tasks.golden | 110 | ||||
| -rw-r--r-- | test/golden/relation-notation/glossing.golden | 111 | ||||
| -rw-r--r-- | test/golden/relation-notation/verification.golden | 11 |
4 files changed, 0 insertions, 233 deletions
diff --git a/test/golden/relation-notation/encoding tasks.golden b/test/golden/relation-notation/encoding tasks.golden deleted file mode 100644 index 8ae6ed7..0000000 --- a/test/golden/relation-notation/encoding tasks.golden +++ /dev/null @@ -1 +0,0 @@ -fof(zf_q0,conjecture,zf_u1(zf_u0(zf_f1,zf_f2),zf_f0)=>zf_u1(zf_u0(zf_f1,zf_f2),zf_f0)).
\ No newline at end of file diff --git a/test/golden/relation-notation/generating tasks.golden b/test/golden/relation-notation/generating tasks.golden deleted file mode 100644 index c584d73..0000000 --- a/test/golden/relation-notation/generating tasks.golden +++ /dev/null @@ -1,110 +0,0 @@ -[ Task - { taskDirectness = Direct - , taskHypotheses = [] - , taskConjectureLabel = Marker "mathrel_notation_test" - , taskLocation = Location - { locFile = "test/examples/relation-notation.tex" - , locLine = 1 - , locColumn = 1 - } - , taskConjecture = Connected Implication - ( TermSymbol - ( Location - { locFile = "test/examples/relation-notation.tex" - , locLine = 2 - , locColumn = 10 - } - ) - ( SymbolPredicate - ( PredicateRelation - ( RelationSymbol - ( Command "in" ) - ( ParameterArity 0 ) - ( Marker "elem" ) - ) - ) - ) - [ TermSymbol - ( Location - { locFile = "test/examples/relation-notation.tex" - , locLine = 2 - , locColumn = 10 - } - ) - ( SymbolMixfix - ( MixfixItem - ( TokenCons - ( Command "pair" ) - ( TokenCons InvisibleBraceL - ( HoleCons - ( TokenCons InvisibleBraceR - ( TokenCons InvisibleBraceL - ( HoleCons ( TokenCons InvisibleBraceR End ) ) - ) - ) - ) - ) - ) - ( Marker "pair" ) NonAssoc - ) - ) - [ TermVar - ( NamedVar "x" ) - , TermVar - ( NamedVar "y" ) - ] - , TermVar - ( NamedVar "R" ) - ] - ) - ( TermSymbol - ( Location - { locFile = "test/examples/relation-notation.tex" - , locLine = 2 - , locColumn = 33 - } - ) - ( SymbolPredicate - ( PredicateRelation - ( RelationSymbol - ( Command "in" ) - ( ParameterArity 0 ) - ( Marker "elem" ) - ) - ) - ) - [ TermSymbol - ( Location - { locFile = "test/examples/relation-notation.tex" - , locLine = 2 - , locColumn = 33 - } - ) - ( SymbolMixfix - ( MixfixItem - ( TokenCons - ( Command "pair" ) - ( TokenCons InvisibleBraceL - ( HoleCons - ( TokenCons InvisibleBraceR - ( TokenCons InvisibleBraceL - ( HoleCons ( TokenCons InvisibleBraceR End ) ) - ) - ) - ) - ) - ) - ( Marker "pair" ) NonAssoc - ) - ) - [ TermVar - ( NamedVar "x" ) - , TermVar - ( NamedVar "y" ) - ] - , TermVar - ( NamedVar "R" ) - ] - ) - } -]
\ No newline at end of file diff --git a/test/golden/relation-notation/glossing.golden b/test/golden/relation-notation/glossing.golden deleted file mode 100644 index 7ce7ed2..0000000 --- a/test/golden/relation-notation/glossing.golden +++ /dev/null @@ -1,111 +0,0 @@ -[ BlockLemma - ( Location - { locFile = "test/examples/relation-notation.tex" - , locLine = 1 - , locColumn = 1 - } - ) - ( Marker "mathrel_notation_test" ) - ( Lemma [] - ( Connected Implication - ( TermSymbol - ( Location - { locFile = "test/examples/relation-notation.tex" - , locLine = 2 - , locColumn = 10 - } - ) - ( SymbolPredicate - ( PredicateRelation - ( RelationSymbol - ( Command "in" ) - ( ParameterArity 0 ) - ( Marker "elem" ) - ) - ) - ) - [ TermSymbol - ( Location - { locFile = "test/examples/relation-notation.tex" - , locLine = 2 - , locColumn = 10 - } - ) - ( SymbolMixfix - ( MixfixItem - ( TokenCons - ( Command "pair" ) - ( TokenCons InvisibleBraceL - ( HoleCons - ( TokenCons InvisibleBraceR - ( TokenCons InvisibleBraceL - ( HoleCons ( TokenCons InvisibleBraceR End ) ) - ) - ) - ) - ) - ) - ( Marker "pair" ) NonAssoc - ) - ) - [ TermVar - ( NamedVar "x" ) - , TermVar - ( NamedVar "y" ) - ] - , TermVar - ( NamedVar "R" ) - ] - ) - ( TermSymbol - ( Location - { locFile = "test/examples/relation-notation.tex" - , locLine = 2 - , locColumn = 33 - } - ) - ( SymbolPredicate - ( PredicateRelation - ( RelationSymbol - ( Command "in" ) - ( ParameterArity 0 ) - ( Marker "elem" ) - ) - ) - ) - [ TermSymbol - ( Location - { locFile = "test/examples/relation-notation.tex" - , locLine = 2 - , locColumn = 33 - } - ) - ( SymbolMixfix - ( MixfixItem - ( TokenCons - ( Command "pair" ) - ( TokenCons InvisibleBraceL - ( HoleCons - ( TokenCons InvisibleBraceR - ( TokenCons InvisibleBraceL - ( HoleCons ( TokenCons InvisibleBraceR End ) ) - ) - ) - ) - ) - ) - ( Marker "pair" ) NonAssoc - ) - ) - [ TermVar - ( NamedVar "x" ) - , TermVar - ( NamedVar "y" ) - ] - , TermVar - ( NamedVar "R" ) - ] - ) - ) - ) -]
\ No newline at end of file diff --git a/test/golden/relation-notation/verification.golden b/test/golden/relation-notation/verification.golden deleted file mode 100644 index b021015..0000000 --- a/test/golden/relation-notation/verification.golden +++ /dev/null @@ -1,11 +0,0 @@ -VerifiedWithTrustedVampire - ( VerificationReport - { verificationRoute = LegacyVerificationRoute - , verificationLegacyDeclaredAssumptionCount = 0 - , verificationTypedDeclaredAssumptionCount = 0 - , verificationTrustedVampireCount = 1 - , verificationExplicitGapLocations = [] - , verificationTrustedLegacyRuleCount = 0 - , verificationKernelProofCount = 0 - } - )
\ No newline at end of file |