summaryrefslogtreecommitdiff
path: root/test/golden/byRef
diff options
context:
space:
mode:
Diffstat (limited to 'test/golden/byRef')
-rw-r--r--test/golden/byRef/encoding tasks.golden22
-rw-r--r--test/golden/byRef/generating tasks.golden519
-rw-r--r--test/golden/byRef/glossing.golden245
-rw-r--r--test/golden/byRef/verification.golden11
4 files changed, 0 insertions, 797 deletions
diff --git a/test/golden/byRef/encoding tasks.golden b/test/golden/byRef/encoding tasks.golden
deleted file mode 100644
index 8a406af..0000000
--- a/test/golden/byRef/encoding tasks.golden
+++ /dev/null
@@ -1,22 +0,0 @@
-fof(zf_q0,conjecture,zf_f0=zf_f0).
-------------------
-fof(zf_q0,conjecture,zf_f0=zf_f0).
-fof(zf_h0,axiom,![V0]:V0=V0).
-------------------
-fof(zf_q0,conjecture,zf_f0=zf_f0).
-fof(zf_h0,axiom,![V0]:V0=V0).
-------------------
-fof(zf_q0,conjecture,![V0]:V0=V0).
-fof(zf_h0,axiom,![V1]:V1=V1).
-------------------
-fof(zf_q0,conjecture,zf_f0=zf_f0).
-fof(zf_h0,axiom,![V0]:V0=V0).
-fof(zf_h1,axiom,![V1]:V1=V1).
-fof(zf_h2,axiom,![V2]:V2=V2).
-fof(zf_h3,axiom,![V3]:V3=V3).
-------------------
-fof(zf_q0,conjecture,zf_f0=zf_f0).
-fof(zf_h0,axiom,![V0]:V0=V0).
-fof(zf_h1,axiom,![V1]:V1=V1).
-fof(zf_h2,axiom,![V2]:V2=V2).
-fof(zf_h3,axiom,![V3]:V3=V3). \ No newline at end of file
diff --git a/test/golden/byRef/generating tasks.golden b/test/golden/byRef/generating tasks.golden
deleted file mode 100644
index 8e80b28..0000000
--- a/test/golden/byRef/generating tasks.golden
+++ /dev/null
@@ -1,519 +0,0 @@
-[ Task
- { taskDirectness = Direct
- , taskHypotheses = []
- , taskConjectureLabel = Marker "prop1"
- , taskLocation = Location
- { locFile = "test/examples/byRef.tex"
- , locLine = 1
- , locColumn = 1
- }
- , taskConjecture = TermSymbol
- ( Location
- { locFile = "test/examples/byRef.tex"
- , locLine = 2
- , locColumn = 8
- }
- )
- ( SymbolPredicate
- ( PredicateRelation
- ( RelationSymbol
- ( Symbol "=" )
- ( ParameterArity 0 )
- ( Marker "eq" )
- )
- )
- )
- [ TermVar
- ( NamedVar "a" )
- , TermVar
- ( NamedVar "a" )
- ]
- }
-, Task
- { taskDirectness = Direct
- , taskHypotheses =
- [ Hypothesis Marker "prop1" Quantified Universally
- ( Scope
- ( TermSymbol
- ( Location
- { locFile = "test/examples/byRef.tex"
- , locLine = 2
- , locColumn = 8
- }
- )
- ( SymbolPredicate
- ( PredicateRelation
- ( RelationSymbol
- ( Symbol "=" )
- ( ParameterArity 0 )
- ( Marker "eq" )
- )
- )
- )
- [ TermVar
- ( B
- ( NamedVar "a" )
- )
- , TermVar
- ( B
- ( NamedVar "a" )
- )
- ]
- )
- )
- ]
- , taskConjectureLabel = Marker "prop2"
- , taskLocation = Location
- { locFile = "test/examples/byRef.tex"
- , locLine = 5
- , locColumn = 1
- }
- , taskConjecture = TermSymbol
- ( Location
- { locFile = "test/examples/byRef.tex"
- , locLine = 6
- , locColumn = 8
- }
- )
- ( SymbolPredicate
- ( PredicateRelation
- ( RelationSymbol
- ( Symbol "=" )
- ( ParameterArity 0 )
- ( Marker "eq" )
- )
- )
- )
- [ TermVar
- ( NamedVar "b" )
- , TermVar
- ( NamedVar "b" )
- ]
- }
-, Task
- { taskDirectness = Direct
- , taskHypotheses =
- [ Hypothesis Marker "prop1" Quantified Universally
- ( Scope
- ( TermSymbol
- ( Location
- { locFile = "test/examples/byRef.tex"
- , locLine = 2
- , locColumn = 8
- }
- )
- ( SymbolPredicate
- ( PredicateRelation
- ( RelationSymbol
- ( Symbol "=" )
- ( ParameterArity 0 )
- ( Marker "eq" )
- )
- )
- )
- [ TermVar
- ( B
- ( NamedVar "a" )
- )
- , TermVar
- ( B
- ( NamedVar "a" )
- )
- ]
- )
- )
- ]
- , taskConjectureLabel = Marker "prop3"
- , taskLocation = Location
- { locFile = "test/examples/byRef.tex"
- , locLine = 13
- , locColumn = 5
- }
- , taskConjecture = TermSymbol
- ( Location
- { locFile = "test/examples/byRef.tex"
- , locLine = 10
- , locColumn = 8
- }
- )
- ( SymbolPredicate
- ( PredicateRelation
- ( RelationSymbol
- ( Symbol "=" )
- ( ParameterArity 0 )
- ( Marker "eq" )
- )
- )
- )
- [ TermVar
- ( NamedVar "c" )
- , TermVar
- ( NamedVar "c" )
- ]
- }
-, Task
- { taskDirectness = Direct
- , taskHypotheses =
- [ Hypothesis Marker "prop1" Quantified Universally
- ( Scope
- ( TermSymbol
- ( Location
- { locFile = "test/examples/byRef.tex"
- , locLine = 2
- , locColumn = 8
- }
- )
- ( SymbolPredicate
- ( PredicateRelation
- ( RelationSymbol
- ( Symbol "=" )
- ( ParameterArity 0 )
- ( Marker "eq" )
- )
- )
- )
- [ TermVar
- ( B
- ( NamedVar "a" )
- )
- , TermVar
- ( B
- ( NamedVar "a" )
- )
- ]
- )
- )
- ]
- , taskConjectureLabel = Marker "prop4"
- , taskLocation = Location
- { locFile = "test/examples/byRef.tex"
- , locLine = 20
- , locColumn = 5
- }
- , taskConjecture = Quantified Universally
- ( Scope
- ( TermSymbol
- ( Location
- { locFile = "test/examples/byRef.tex"
- , locLine = 20
- , locColumn = 28
- }
- )
- ( SymbolPredicate
- ( PredicateRelation
- ( RelationSymbol
- ( Symbol "=" )
- ( ParameterArity 0 )
- ( Marker "eq" )
- )
- )
- )
- [ TermVar
- ( B
- ( NamedVar "d" )
- )
- , TermVar
- ( B
- ( NamedVar "d" )
- )
- ]
- )
- )
- }
-, Task
- { taskDirectness = Direct
- , taskHypotheses =
- [ Hypothesis Marker "prop3" Quantified Universally
- ( Scope
- ( TermSymbol
- ( Location
- { locFile = "test/examples/byRef.tex"
- , locLine = 10
- , locColumn = 8
- }
- )
- ( SymbolPredicate
- ( PredicateRelation
- ( RelationSymbol
- ( Symbol "=" )
- ( ParameterArity 0 )
- ( Marker "eq" )
- )
- )
- )
- [ TermVar
- ( B
- ( NamedVar "c" )
- )
- , TermVar
- ( B
- ( NamedVar "c" )
- )
- ]
- )
- )
- , Hypothesis Marker "prop2" Quantified Universally
- ( Scope
- ( TermSymbol
- ( Location
- { locFile = "test/examples/byRef.tex"
- , locLine = 6
- , locColumn = 8
- }
- )
- ( SymbolPredicate
- ( PredicateRelation
- ( RelationSymbol
- ( Symbol "=" )
- ( ParameterArity 0 )
- ( Marker "eq" )
- )
- )
- )
- [ TermVar
- ( B
- ( NamedVar "b" )
- )
- , TermVar
- ( B
- ( NamedVar "b" )
- )
- ]
- )
- )
- , Hypothesis Marker "prop1" Quantified Universally
- ( Scope
- ( TermSymbol
- ( Location
- { locFile = "test/examples/byRef.tex"
- , locLine = 2
- , locColumn = 8
- }
- )
- ( SymbolPredicate
- ( PredicateRelation
- ( RelationSymbol
- ( Symbol "=" )
- ( ParameterArity 0 )
- ( Marker "eq" )
- )
- )
- )
- [ TermVar
- ( B
- ( NamedVar "a" )
- )
- , TermVar
- ( B
- ( NamedVar "a" )
- )
- ]
- )
- )
- , Hypothesis Marker "_local_1" Quantified Universally
- ( Scope
- ( TermSymbol
- ( Location
- { locFile = "test/examples/byRef.tex"
- , locLine = 20
- , locColumn = 28
- }
- )
- ( SymbolPredicate
- ( PredicateRelation
- ( RelationSymbol
- ( Symbol "=" )
- ( ParameterArity 0 )
- ( Marker "eq" )
- )
- )
- )
- [ TermVar
- ( B
- ( NamedVar "d" )
- )
- , TermVar
- ( B
- ( NamedVar "d" )
- )
- ]
- )
- )
- ]
- , taskConjectureLabel = Marker "prop4"
- , taskLocation = Location
- { locFile = "test/examples/byRef.tex"
- , locLine = 21
- , locColumn = 1
- }
- , taskConjecture = TermSymbol
- ( Location
- { locFile = "test/examples/byRef.tex"
- , locLine = 17
- , locColumn = 8
- }
- )
- ( SymbolPredicate
- ( PredicateRelation
- ( RelationSymbol
- ( Symbol "=" )
- ( ParameterArity 0 )
- ( Marker "eq" )
- )
- )
- )
- [ TermVar
- ( NamedVar "e" )
- , TermVar
- ( NamedVar "e" )
- ]
- }
-, Task
- { taskDirectness = Direct
- , taskHypotheses =
- [ Hypothesis Marker "prop4" Quantified Universally
- ( Scope
- ( TermSymbol
- ( Location
- { locFile = "test/examples/byRef.tex"
- , locLine = 17
- , locColumn = 8
- }
- )
- ( SymbolPredicate
- ( PredicateRelation
- ( RelationSymbol
- ( Symbol "=" )
- ( ParameterArity 0 )
- ( Marker "eq" )
- )
- )
- )
- [ TermVar
- ( B
- ( NamedVar "e" )
- )
- , TermVar
- ( B
- ( NamedVar "e" )
- )
- ]
- )
- )
- , Hypothesis Marker "prop3" Quantified Universally
- ( Scope
- ( TermSymbol
- ( Location
- { locFile = "test/examples/byRef.tex"
- , locLine = 10
- , locColumn = 8
- }
- )
- ( SymbolPredicate
- ( PredicateRelation
- ( RelationSymbol
- ( Symbol "=" )
- ( ParameterArity 0 )
- ( Marker "eq" )
- )
- )
- )
- [ TermVar
- ( B
- ( NamedVar "c" )
- )
- , TermVar
- ( B
- ( NamedVar "c" )
- )
- ]
- )
- )
- , Hypothesis Marker "prop2" Quantified Universally
- ( Scope
- ( TermSymbol
- ( Location
- { locFile = "test/examples/byRef.tex"
- , locLine = 6
- , locColumn = 8
- }
- )
- ( SymbolPredicate
- ( PredicateRelation
- ( RelationSymbol
- ( Symbol "=" )
- ( ParameterArity 0 )
- ( Marker "eq" )
- )
- )
- )
- [ TermVar
- ( B
- ( NamedVar "b" )
- )
- , TermVar
- ( B
- ( NamedVar "b" )
- )
- ]
- )
- )
- , Hypothesis Marker "prop1" Quantified Universally
- ( Scope
- ( TermSymbol
- ( Location
- { locFile = "test/examples/byRef.tex"
- , locLine = 2
- , locColumn = 8
- }
- )
- ( SymbolPredicate
- ( PredicateRelation
- ( RelationSymbol
- ( Symbol "=" )
- ( ParameterArity 0 )
- ( Marker "eq" )
- )
- )
- )
- [ TermVar
- ( B
- ( NamedVar "a" )
- )
- , TermVar
- ( B
- ( NamedVar "a" )
- )
- ]
- )
- )
- ]
- , taskConjectureLabel = Marker "prop5"
- , taskLocation = Location
- { locFile = "test/examples/byRef.tex"
- , locLine = 23
- , locColumn = 1
- }
- , taskConjecture = TermSymbol
- ( Location
- { locFile = "test/examples/byRef.tex"
- , locLine = 24
- , locColumn = 8
- }
- )
- ( SymbolPredicate
- ( PredicateRelation
- ( RelationSymbol
- ( Symbol "=" )
- ( ParameterArity 0 )
- ( Marker "eq" )
- )
- )
- )
- [ TermVar
- ( NamedVar "f" )
- , TermVar
- ( NamedVar "f" )
- ]
- }
-] \ No newline at end of file
diff --git a/test/golden/byRef/glossing.golden b/test/golden/byRef/glossing.golden
deleted file mode 100644
index 0af8bbb..0000000
--- a/test/golden/byRef/glossing.golden
+++ /dev/null
@@ -1,245 +0,0 @@
-[ BlockLemma
- ( Location
- { locFile = "test/examples/byRef.tex"
- , locLine = 1
- , locColumn = 1
- }
- )
- ( Marker "prop1" )
- ( Lemma []
- ( TermSymbol
- ( Location
- { locFile = "test/examples/byRef.tex"
- , locLine = 2
- , locColumn = 8
- }
- )
- ( SymbolPredicate
- ( PredicateRelation
- ( RelationSymbol
- ( Symbol "=" )
- ( ParameterArity 0 )
- ( Marker "eq" )
- )
- )
- )
- [ TermVar
- ( NamedVar "a" )
- , TermVar
- ( NamedVar "a" )
- ]
- )
- )
-, BlockLemma
- ( Location
- { locFile = "test/examples/byRef.tex"
- , locLine = 5
- , locColumn = 1
- }
- )
- ( Marker "prop2" )
- ( Lemma []
- ( TermSymbol
- ( Location
- { locFile = "test/examples/byRef.tex"
- , locLine = 6
- , locColumn = 8
- }
- )
- ( SymbolPredicate
- ( PredicateRelation
- ( RelationSymbol
- ( Symbol "=" )
- ( ParameterArity 0 )
- ( Marker "eq" )
- )
- )
- )
- [ TermVar
- ( NamedVar "b" )
- , TermVar
- ( NamedVar "b" )
- ]
- )
- )
-, BlockLemma
- ( Location
- { locFile = "test/examples/byRef.tex"
- , locLine = 9
- , locColumn = 1
- }
- )
- ( Marker "prop3" )
- ( Lemma []
- ( TermSymbol
- ( Location
- { locFile = "test/examples/byRef.tex"
- , locLine = 10
- , locColumn = 8
- }
- )
- ( SymbolPredicate
- ( PredicateRelation
- ( RelationSymbol
- ( Symbol "=" )
- ( ParameterArity 0 )
- ( Marker "eq" )
- )
- )
- )
- [ TermVar
- ( NamedVar "c" )
- , TermVar
- ( NamedVar "c" )
- ]
- )
- )
-, BlockProof
- ( Location
- { locFile = "test/examples/byRef.tex"
- , locLine = 12
- , locColumn = 1
- }
- )
- ( Location
- { locFile = "test/examples/byRef.tex"
- , locLine = 14
- , locColumn = 1
- }
- )
- ( Qed
- { mloc = Just
- ( Location
- { locFile = "test/examples/byRef.tex"
- , locLine = 13
- , locColumn = 5
- }
- )
- , by = JustificationRef
- ( Marker "prop1" :| [] )
- }
- )
-, BlockLemma
- ( Location
- { locFile = "test/examples/byRef.tex"
- , locLine = 16
- , locColumn = 1
- }
- )
- ( Marker "prop4" )
- ( Lemma []
- ( TermSymbol
- ( Location
- { locFile = "test/examples/byRef.tex"
- , locLine = 17
- , locColumn = 8
- }
- )
- ( SymbolPredicate
- ( PredicateRelation
- ( RelationSymbol
- ( Symbol "=" )
- ( ParameterArity 0 )
- ( Marker "eq" )
- )
- )
- )
- [ TermVar
- ( NamedVar "e" )
- , TermVar
- ( NamedVar "e" )
- ]
- )
- )
-, BlockProof
- ( Location
- { locFile = "test/examples/byRef.tex"
- , locLine = 19
- , locColumn = 1
- }
- )
- ( Location
- { locFile = "test/examples/byRef.tex"
- , locLine = 21
- , locColumn = 1
- }
- )
- ( Have
- ( Location
- { locFile = "test/examples/byRef.tex"
- , locLine = 20
- , locColumn = 5
- }
- )
- ( Quantified Universally
- ( Scope
- ( TermSymbol
- ( Location
- { locFile = "test/examples/byRef.tex"
- , locLine = 20
- , locColumn = 28
- }
- )
- ( SymbolPredicate
- ( PredicateRelation
- ( RelationSymbol
- ( Symbol "=" )
- ( ParameterArity 0 )
- ( Marker "eq" )
- )
- )
- )
- [ TermVar
- ( B
- ( NamedVar "d" )
- )
- , TermVar
- ( B
- ( NamedVar "d" )
- )
- ]
- )
- )
- )
- ( JustificationRef
- ( Marker "prop1" :| [] )
- )
- ( Qed
- { mloc = Nothing
- , by = JustificationEmpty
- }
- )
- )
-, BlockLemma
- ( Location
- { locFile = "test/examples/byRef.tex"
- , locLine = 23
- , locColumn = 1
- }
- )
- ( Marker "prop5" )
- ( Lemma []
- ( TermSymbol
- ( Location
- { locFile = "test/examples/byRef.tex"
- , locLine = 24
- , locColumn = 8
- }
- )
- ( SymbolPredicate
- ( PredicateRelation
- ( RelationSymbol
- ( Symbol "=" )
- ( ParameterArity 0 )
- ( Marker "eq" )
- )
- )
- )
- [ TermVar
- ( NamedVar "f" )
- , TermVar
- ( NamedVar "f" )
- ]
- )
- )
-] \ No newline at end of file
diff --git a/test/golden/byRef/verification.golden b/test/golden/byRef/verification.golden
deleted file mode 100644
index 9b3d1de..0000000
--- a/test/golden/byRef/verification.golden
+++ /dev/null
@@ -1,11 +0,0 @@
-VerifiedWithTrustedVampire
- ( VerificationReport
- { verificationRoute = LegacyVerificationRoute
- , verificationLegacyDeclaredAssumptionCount = 0
- , verificationTypedDeclaredAssumptionCount = 0
- , verificationTrustedVampireCount = 6
- , verificationExplicitGapLocations = []
- , verificationTrustedLegacyRuleCount = 1
- , verificationKernelProofCount = 0
- }
- ) \ No newline at end of file
generated by cgit v1.2.3 (git 2.39.1) at 2026-08-05 01:47:37 +0000