diff options
Diffstat (limited to 'test/golden/inductive')
| -rw-r--r-- | test/golden/inductive/encoding tasks.golden | 1 | ||||
| -rw-r--r-- | test/golden/inductive/generating tasks.golden | 59 | ||||
| -rw-r--r-- | test/golden/inductive/glossing.golden | 86 | ||||
| -rw-r--r-- | test/golden/inductive/verification.golden | 11 |
4 files changed, 0 insertions, 157 deletions
diff --git a/test/golden/inductive/encoding tasks.golden b/test/golden/inductive/encoding tasks.golden deleted file mode 100644 index af2aad1..0000000 --- a/test/golden/inductive/encoding tasks.golden +++ /dev/null @@ -1 +0,0 @@ -fof(zf_q0,conjecture,![V0]:zf_u1(V0,zf_u0(V0))).
\ No newline at end of file diff --git a/test/golden/inductive/generating tasks.golden b/test/golden/inductive/generating tasks.golden deleted file mode 100644 index 18cb929..0000000 --- a/test/golden/inductive/generating tasks.golden +++ /dev/null @@ -1,59 +0,0 @@ -[ Task - { taskDirectness = Direct - , taskHypotheses = [] - , taskConjectureLabel = Marker "fin" - , taskLocation = Location - { locFile = "test/examples/inductive.tex" - , locLine = 3 - , locColumn = 1 - } - , taskConjecture = Quantified Universally - ( Scope - ( TermSymbol - ( Location - { locFile = "<nowhere>" - , locLine = -1 - , locColumn = -1 - } - ) - ( SymbolPredicate - ( PredicateRelation - ( RelationSymbol - ( Command "in" ) - ( ParameterArity 0 ) - ( Marker "elem" ) - ) - ) - ) - [ TermVar - ( B - ( NamedVar "A" ) - ) - , TermSymbol - ( Location - { locFile = "test/examples/inductive.tex" - , locLine = 4 - , locColumn = 29 - } - ) - ( SymbolMixfix - ( MixfixItem - ( TokenCons - ( Command "cumul" ) - ( TokenCons InvisibleBraceL - ( HoleCons ( TokenCons InvisibleBraceR End ) ) - ) - ) - ( Marker "cumul" ) NonAssoc - ) - ) - [ TermVar - ( B - ( NamedVar "A" ) - ) - ] - ] - ) - ) - } -]
\ No newline at end of file diff --git a/test/golden/inductive/glossing.golden b/test/golden/inductive/glossing.golden deleted file mode 100644 index 98f60e8..0000000 --- a/test/golden/inductive/glossing.golden +++ /dev/null @@ -1,86 +0,0 @@ -[ BlockInductive - ( Location - { locFile = "test/examples/inductive.tex" - , locLine = 3 - , locColumn = 1 - } - ) - ( Marker "fin" ) - ( Inductive - { inductiveSymbol = MixfixItem - ( TokenCons - ( Command "fin" ) - ( TokenCons InvisibleBraceL - ( HoleCons ( TokenCons InvisibleBraceR End ) ) - ) - ) - ( Marker "fin" ) NonAssoc - , inductiveParams = - [ NamedVar "A" ] - , inductiveDomain = TermSymbol - ( Location - { locFile = "test/examples/inductive.tex" - , locLine = 4 - , locColumn = 29 - } - ) - ( SymbolMixfix - ( MixfixItem - ( TokenCons - ( Command "cumul" ) - ( TokenCons InvisibleBraceL - ( HoleCons ( TokenCons InvisibleBraceR End ) ) - ) - ) - ( Marker "cumul" ) NonAssoc - ) - ) - [ TermVar - ( NamedVar "A" ) - ] - , inductiveIntros = IntroRule - { introConditions = [] - , introResult = TermSymbol - ( Location - { locFile = "test/examples/inductive.tex" - , locLine = 6 - , locColumn = 17 - } - ) - ( SymbolPredicate - ( PredicateRelation - ( RelationSymbol - ( Command "in" ) - ( ParameterArity 0 ) - ( Marker "elem" ) - ) - ) - ) - [ TermVar - ( NamedVar "A" ) - , TermSymbol - ( Location - { locFile = "test/examples/inductive.tex" - , locLine = 6 - , locColumn = 20 - } - ) - ( SymbolMixfix - ( MixfixItem - ( TokenCons - ( Command "fin" ) - ( TokenCons InvisibleBraceL - ( HoleCons ( TokenCons InvisibleBraceR End ) ) - ) - ) - ( Marker "fin" ) NonAssoc - ) - ) - [ TermVar - ( NamedVar "A" ) - ] - ] - } :| [] - } - ) -]
\ No newline at end of file diff --git a/test/golden/inductive/verification.golden b/test/golden/inductive/verification.golden deleted file mode 100644 index f9813a5..0000000 --- a/test/golden/inductive/verification.golden +++ /dev/null @@ -1,11 +0,0 @@ -VerifiedWithTrustedVampire - ( VerificationReport - { verificationRoute = LegacyVerificationRoute - , verificationLegacyDeclaredAssumptionCount = 0 - , verificationTypedDeclaredAssumptionCount = 0 - , verificationTrustedVampireCount = 0 - , verificationExplicitGapLocations = [] - , verificationTrustedLegacyRuleCount = 0 - , verificationKernelProofCount = 4 - } - )
\ No newline at end of file |