summaryrefslogtreecommitdiff
path: root/test/golden/proofdefinefunction/generating tasks.golden
diff options
context:
space:
mode:
Diffstat (limited to 'test/golden/proofdefinefunction/generating tasks.golden')
-rw-r--r--test/golden/proofdefinefunction/generating tasks.golden473
1 files changed, 0 insertions, 473 deletions
diff --git a/test/golden/proofdefinefunction/generating tasks.golden b/test/golden/proofdefinefunction/generating tasks.golden
deleted file mode 100644
index 9573633..0000000
--- a/test/golden/proofdefinefunction/generating tasks.golden
+++ /dev/null
@@ -1,473 +0,0 @@
-[ Task
- { taskDirectness = Direct
- , taskHypotheses =
- [ Hypothesis Marker "relation" Quantified Universally
- ( Scope
- ( Connected Equivalence
- ( TermSymbol
- ( Location
- { locFile = "test/examples/proofdefinefunction.tex"
- , locLine = 18
- , locColumn = 1
- }
- )
- ( SymbolPredicate
- ( PredicateNoun
- ( LexicalItemSgPl
- ( SgPl
- { sg = TokenCons
- ( Word "relation" ) End
- , pl = TokenCons
- ( Word "relations" ) End
- }
- )
- ( Marker "relation" )
- )
- )
- )
- [ TermVar
- ( B
- ( NamedVar "f" )
- )
- ]
- )
- ( Quantified Universally
- ( Scope
- ( TermSymbol
- ( Location
- { locFile = "test/examples/proofdefinefunction.tex"
- , locLine = 19
- , locColumn = 29
- }
- )
- ( SymbolPredicate
- ( PredicateRelation
- ( RelationSymbol
- ( Symbol "=" )
- ( ParameterArity 0 )
- ( Marker "eq" )
- )
- )
- )
- [ TermVar
- ( F
- ( TermVar
- ( B
- ( NamedVar "f" )
- )
- )
- )
- , TermVar
- ( F
- ( TermVar
- ( B
- ( NamedVar "f" )
- )
- )
- )
- ]
- )
- )
- )
- )
- )
- , Hypothesis Marker "rightunique" Quantified Universally
- ( Scope
- ( Connected Equivalence
- ( TermSymbol
- ( Location
- { locFile = "test/examples/proofdefinefunction.tex"
- , locLine = 13
- , locColumn = 1
- }
- )
- ( SymbolPredicate
- ( PredicateAdj
- ( LexicalItem
- ( TokenCons
- ( Word "right-unique" ) End
- )
- ( Marker "rightunique" )
- )
- )
- )
- [ TermVar
- ( B
- ( NamedVar "f" )
- )
- ]
- )
- ( Quantified Universally
- ( Scope
- ( TermSymbol
- ( Location
- { locFile = "test/examples/proofdefinefunction.tex"
- , locLine = 14
- , locColumn = 31
- }
- )
- ( SymbolPredicate
- ( PredicateRelation
- ( RelationSymbol
- ( Symbol "=" )
- ( ParameterArity 0 )
- ( Marker "eq" )
- )
- )
- )
- [ TermVar
- ( F
- ( TermVar
- ( B
- ( NamedVar "f" )
- )
- )
- )
- , TermVar
- ( F
- ( TermVar
- ( B
- ( NamedVar "f" )
- )
- )
- )
- ]
- )
- )
- )
- )
- )
- , Hypothesis Marker "dom" Quantified Universally
- ( Scope
- ( TermSymbol
- ( Location
- { locFile = "<nowhere>"
- , locLine = -1
- , locColumn = -1
- }
- )
- ( SymbolPredicate
- ( PredicateRelation
- ( RelationSymbol
- ( Symbol "=" )
- ( ParameterArity 0 )
- ( Marker "eq" )
- )
- )
- )
- [ TermSymbol
- ( Location
- { locFile = "<nowhere>"
- , locLine = -1
- , locColumn = -1
- }
- )
- ( SymbolMixfix
- ( MixfixItem
- ( TokenCons
- ( Command "dom" )
- ( TokenCons InvisibleBraceL
- ( HoleCons ( TokenCons InvisibleBraceR End ) )
- )
- )
- ( Marker "dom" ) NonAssoc
- )
- )
- [ TermVar
- ( B
- ( NamedVar "f" )
- )
- ]
- , TermVar
- ( B
- ( NamedVar "f" )
- )
- ]
- )
- )
- , Hypothesis Marker "apply" Quantified Universally
- ( Scope
- ( TermSymbol
- ( Location
- { locFile = "<nowhere>"
- , locLine = -1
- , locColumn = -1
- }
- )
- ( SymbolPredicate
- ( PredicateRelation
- ( RelationSymbol
- ( Symbol "=" )
- ( ParameterArity 0 )
- ( Marker "eq" )
- )
- )
- )
- [ TermSymbol
- ( Location
- { locFile = "<nowhere>"
- , locLine = -1
- , locColumn = -1
- }
- )
- ( SymbolMixfix
- ( MixfixItem
- ( TokenCons
- ( Command "apply" )
- ( TokenCons InvisibleBraceL
- ( HoleCons
- ( TokenCons InvisibleBraceR
- ( TokenCons InvisibleBraceL
- ( HoleCons ( TokenCons InvisibleBraceR End ) )
- )
- )
- )
- )
- )
- ( Marker "apply" ) NonAssoc
- )
- )
- [ TermVar
- ( B
- ( NamedVar "f" )
- )
- , TermVar
- ( B
- ( NamedVar "x" )
- )
- ]
- , TermVar
- ( B
- ( NamedVar "x" )
- )
- ]
- )
- )
- , Hypothesis Marker "_local_4" TermSymbol
- ( Location
- { locFile = "test/examples/proofdefinefunction.tex"
- , locLine = 26
- , locColumn = 5
- }
- )
- ( SymbolPredicate
- ( PredicateNoun
- ( LexicalItemSgPl
- ( SgPl
- { sg = TokenCons
- ( Word "relation" ) End
- , pl = TokenCons
- ( Word "relations" ) End
- }
- )
- ( Marker "relation" )
- )
- )
- )
- [ TermVar
- ( NamedVar "f" )
- ]
- , Hypothesis Marker "_local_3" TermSymbol
- ( Location
- { locFile = "test/examples/proofdefinefunction.tex"
- , locLine = 26
- , locColumn = 5
- }
- )
- ( SymbolPredicate
- ( PredicateAdj
- ( LexicalItem
- ( TokenCons
- ( Word "right-unique" ) End
- )
- ( Marker "rightunique" )
- )
- )
- )
- [ TermVar
- ( NamedVar "f" )
- ]
- , Hypothesis Marker "_local_2" Quantified Universally
- ( Scope
- ( Connected Implication
- ( TermSymbol
- ( Location
- { locFile = "<nowhere>"
- , locLine = -1
- , locColumn = -1
- }
- )
- ( SymbolPredicate
- ( PredicateRelation
- ( RelationSymbol
- ( Command "in" )
- ( ParameterArity 0 )
- ( Marker "elem" )
- )
- )
- )
- [ TermVar
- ( B
- ( NamedVar "z" )
- )
- , TermVar
- ( F
- ( TermVar
- ( NamedVar "x" )
- )
- )
- ]
- )
- ( TermSymbol
- ( Location
- { locFile = "<nowhere>"
- , locLine = -1
- , locColumn = -1
- }
- )
- ( SymbolPredicate
- ( PredicateRelation
- ( RelationSymbol
- ( Symbol "=" )
- ( ParameterArity 0 )
- ( Marker "eq" )
- )
- )
- )
- [ TermSymbol
- ( Location
- { locFile = "<nowhere>"
- , locLine = -1
- , locColumn = -1
- }
- )
- ( SymbolMixfix
- ( MixfixItem
- ( TokenCons
- ( Command "apply" )
- ( TokenCons InvisibleBraceL
- ( HoleCons
- ( TokenCons InvisibleBraceR
- ( TokenCons InvisibleBraceL
- ( HoleCons ( TokenCons InvisibleBraceR End ) )
- )
- )
- )
- )
- )
- ( Marker "apply" ) NonAssoc
- )
- )
- [ TermVar
- ( F
- ( TermVar
- ( NamedVar "f" )
- )
- )
- , TermVar
- ( B
- ( NamedVar "z" )
- )
- ]
- , TermVar
- ( B
- ( NamedVar "z" )
- )
- ]
- )
- )
- )
- , Hypothesis Marker "_local_1" TermSymbol
- ( Location
- { locFile = "test/examples/proofdefinefunction.tex"
- , locLine = 26
- , locColumn = 5
- }
- )
- ( SymbolPredicate
- ( PredicateRelation
- ( RelationSymbol
- ( Symbol "=" )
- ( ParameterArity 0 )
- ( Marker "eq" )
- )
- )
- )
- [ TermSymbol
- ( Location
- { locFile = "<nowhere>"
- , locLine = -1
- , locColumn = -1
- }
- )
- ( SymbolMixfix
- ( MixfixItem
- ( TokenCons
- ( Command "dom" )
- ( TokenCons InvisibleBraceL
- ( HoleCons ( TokenCons InvisibleBraceR End ) )
- )
- )
- ( Marker "dom" ) NonAssoc
- )
- )
- [ TermVar
- ( NamedVar "f" )
- ]
- , TermVar
- ( NamedVar "x" )
- ]
- ]
- , taskConjectureLabel = Marker "definefunctiontest"
- , taskLocation = Location
- { locFile = "test/examples/proofdefinefunction.tex"
- , locLine = 27
- , locColumn = 1
- }
- , taskConjecture = Connected Implication
- ( TermSymbol
- ( Location
- { locFile = "test/examples/proofdefinefunction.tex"
- , locLine = 23
- , locColumn = 10
- }
- )
- ( SymbolPredicate
- ( PredicateRelation
- ( RelationSymbol
- ( Command "in" )
- ( ParameterArity 0 )
- ( Marker "elem" )
- )
- )
- )
- [ TermVar
- ( NamedVar "x" )
- , TermVar
- ( NamedVar "y" )
- ]
- )
- ( TermSymbol
- ( Location
- { locFile = "test/examples/proofdefinefunction.tex"
- , locLine = 23
- , locColumn = 25
- }
- )
- ( SymbolPredicate
- ( PredicateRelation
- ( RelationSymbol
- ( Command "in" )
- ( ParameterArity 0 )
- ( Marker "elem" )
- )
- )
- )
- [ TermVar
- ( NamedVar "x" )
- , TermVar
- ( NamedVar "y" )
- ]
- )
- }
-] \ No newline at end of file
generated by cgit v1.2.3 (git 2.39.1) at 2026-08-04 05:42:34 +0000