summaryrefslogtreecommitdiff
path: root/test/golden/replace/glossing.golden
diff options
context:
space:
mode:
Diffstat (limited to 'test/golden/replace/glossing.golden')
-rw-r--r--test/golden/replace/glossing.golden572
1 files changed, 0 insertions, 572 deletions
diff --git a/test/golden/replace/glossing.golden b/test/golden/replace/glossing.golden
deleted file mode 100644
index dfded02..0000000
--- a/test/golden/replace/glossing.golden
+++ /dev/null
@@ -1,572 +0,0 @@
-[ BlockAxiom
- ( Location
- { locFile = "test/examples/replace.tex"
- , locLine = 1
- , locColumn = 1
- }
- )
- ( Marker "cons" )
- ( Axiom []
- ( Connected Equivalence
- ( TermSymbol
- ( Location
- { locFile = "test/examples/replace.tex"
- , locLine = 2
- , locColumn = 7
- }
- )
- ( SymbolPredicate
- ( PredicateRelation
- ( RelationSymbol
- ( Command "in" )
- ( ParameterArity 0 )
- ( Marker "elem" )
- )
- )
- )
- [ TermVar
- ( NamedVar "x" )
- , TermSymbol
- ( Location
- { locFile = "test/examples/replace.tex"
- , locLine = 2
- , locColumn = 11
- }
- )
- ( SymbolMixfix
- ( MixfixItem
- ( TokenCons
- ( Command "cons" )
- ( TokenCons InvisibleBraceL
- ( HoleCons
- ( TokenCons InvisibleBraceR
- ( TokenCons InvisibleBraceL
- ( HoleCons ( TokenCons InvisibleBraceR End ) )
- )
- )
- )
- )
- )
- ( Marker "cons" ) NonAssoc
- )
- )
- [ TermVar
- ( NamedVar "y" )
- , TermVar
- ( NamedVar "X" )
- ]
- ]
- )
- ( Connected Disjunction
- ( TermSymbol
- ( Location
- { locFile = "test/examples/replace.tex"
- , locLine = 2
- , locColumn = 31
- }
- )
- ( SymbolPredicate
- ( PredicateRelation
- ( RelationSymbol
- ( Symbol "=" )
- ( ParameterArity 0 )
- ( Marker "eq" )
- )
- )
- )
- [ TermVar
- ( NamedVar "x" )
- , TermVar
- ( NamedVar "y" )
- ]
- )
- ( TermSymbol
- ( Location
- { locFile = "test/examples/replace.tex"
- , locLine = 2
- , locColumn = 41
- }
- )
- ( SymbolPredicate
- ( PredicateRelation
- ( RelationSymbol
- ( Command "in" )
- ( ParameterArity 0 )
- ( Marker "elem" )
- )
- )
- )
- [ TermVar
- ( NamedVar "x" )
- , TermVar
- ( NamedVar "X" )
- ]
- )
- )
- )
- )
-, BlockDefn
- ( Location
- { locFile = "test/examples/replace.tex"
- , locLine = 5
- , locColumn = 1
- }
- )
- ( Marker "times" )
- ( DefnOp
- ( MixfixItem
- ( HoleCons
- ( TokenCons
- ( Command "times" ) ( HoleCons End )
- )
- )
- ( Marker "times" ) RightAssoc
- )
- [ NamedVar "A"
- , NamedVar "B"
- ]
- ( ReplaceFun
- (
- ( NamedVar "a"
- , TermVar
- ( NamedVar "A" )
- ) :|
- [
- ( NamedVar "b"
- , TermVar
- ( NamedVar "B" )
- )
- ]
- )
- ( Scope
- ( TermSymbol
- ( Location
- { locFile = "test/examples/replace.tex"
- , locLine = 6
- , locColumn = 21
- }
- )
- ( SymbolMixfix
- ( MixfixItem
- ( TokenCons
- ( Command "pair" )
- ( TokenCons InvisibleBraceL
- ( HoleCons
- ( TokenCons InvisibleBraceR
- ( TokenCons InvisibleBraceL
- ( HoleCons ( TokenCons InvisibleBraceR End ) )
- )
- )
- )
- )
- )
- ( Marker "pair" ) NonAssoc
- )
- )
- [ TermVar
- ( B
- ( NamedVar "a" )
- )
- , TermVar
- ( B
- ( NamedVar "b" )
- )
- ]
- )
- )
- ( Scope ( PropositionalConstant IsTop ) )
- )
- )
-, BlockDefn
- ( Location
- { locFile = "test/examples/replace.tex"
- , locLine = 9
- , locColumn = 1
- }
- )
- ( Marker "unit" )
- ( DefnOp
- ( MixfixItem
- ( TokenCons
- ( Command "unit" ) End
- )
- ( Marker "unit" ) NonAssoc
- ) []
- ( TermSymbol
- ( Location
- { locFile = "test/examples/replace.tex"
- , locLine = 10
- , locColumn = 14
- }
- )
- ( SymbolMixfix
- ( MixfixItem
- ( TokenCons
- ( Command "cons" )
- ( TokenCons InvisibleBraceL
- ( HoleCons
- ( TokenCons InvisibleBraceR
- ( TokenCons InvisibleBraceL
- ( HoleCons ( TokenCons InvisibleBraceR End ) )
- )
- )
- )
- )
- )
- ( Marker "cons" ) NonAssoc
- )
- )
- [ TermSymbol
- ( Location
- { locFile = "test/examples/replace.tex"
- , locLine = 10
- , locColumn = 16
- }
- )
- ( SymbolMixfix
- ( MixfixItem
- ( TokenCons
- ( Command "emptyset" ) End
- )
- ( Marker "emptyset" ) NonAssoc
- )
- ) []
- , TermSymbol
- ( Location
- { locFile = "test/examples/replace.tex"
- , locLine = 10
- , locColumn = 14
- }
- )
- ( SymbolMixfix
- ( MixfixItem
- ( TokenCons
- ( Command "emptyset" ) End
- )
- ( Marker "emptyset" ) NonAssoc
- )
- ) []
- ]
- )
- )
-, BlockLemma
- ( Location
- { locFile = "test/examples/replace.tex"
- , locLine = 13
- , locColumn = 1
- }
- )
- ( Marker "pair_emptyset_in_times_unit" )
- ( Lemma []
- ( TermSymbol
- ( Location
- { locFile = "test/examples/replace.tex"
- , locLine = 14
- , locColumn = 27
- }
- )
- ( SymbolPredicate
- ( PredicateRelation
- ( RelationSymbol
- ( Command "in" )
- ( ParameterArity 0 )
- ( Marker "elem" )
- )
- )
- )
- [ TermSymbol
- ( Location
- { locFile = "test/examples/replace.tex"
- , locLine = 14
- , locColumn = 6
- }
- )
- ( SymbolMixfix
- ( MixfixItem
- ( TokenCons
- ( Command "pair" )
- ( TokenCons InvisibleBraceL
- ( HoleCons
- ( TokenCons InvisibleBraceR
- ( TokenCons InvisibleBraceL
- ( HoleCons ( TokenCons InvisibleBraceR End ) )
- )
- )
- )
- )
- )
- ( Marker "pair" ) NonAssoc
- )
- )
- [ TermSymbol
- ( Location
- { locFile = "test/examples/replace.tex"
- , locLine = 14
- , locColumn = 7
- }
- )
- ( SymbolMixfix
- ( MixfixItem
- ( TokenCons
- ( Command "emptyset" ) End
- )
- ( Marker "emptyset" ) NonAssoc
- )
- ) []
- , TermSymbol
- ( Location
- { locFile = "test/examples/replace.tex"
- , locLine = 14
- , locColumn = 17
- }
- )
- ( SymbolMixfix
- ( MixfixItem
- ( TokenCons
- ( Command "emptyset" ) End
- )
- ( Marker "emptyset" ) NonAssoc
- )
- ) []
- ]
- , TermSymbol
- ( Location
- { locFile = "test/examples/replace.tex"
- , locLine = 14
- , locColumn = 31
- }
- )
- ( SymbolMixfix
- ( MixfixItem
- ( HoleCons
- ( TokenCons
- ( Command "times" ) ( HoleCons End )
- )
- )
- ( Marker "times" ) RightAssoc
- )
- )
- [ TermSymbol
- ( Location
- { locFile = "test/examples/replace.tex"
- , locLine = 14
- , locColumn = 31
- }
- )
- ( SymbolMixfix
- ( MixfixItem
- ( TokenCons
- ( Command "unit" ) End
- )
- ( Marker "unit" ) NonAssoc
- )
- ) []
- , TermSymbol
- ( Location
- { locFile = "test/examples/replace.tex"
- , locLine = 14
- , locColumn = 42
- }
- )
- ( SymbolMixfix
- ( MixfixItem
- ( TokenCons
- ( Command "unit" ) End
- )
- ( Marker "unit" ) NonAssoc
- )
- ) []
- ]
- ]
- )
- )
-, BlockDefn
- ( Location
- { locFile = "test/examples/replace.tex"
- , locLine = 19
- , locColumn = 1
- }
- )
- ( Marker "suc" )
- ( DefnOp
- ( MixfixItem
- ( TokenCons
- ( Command "suc" )
- ( TokenCons InvisibleBraceL
- ( HoleCons ( TokenCons InvisibleBraceR End ) )
- )
- )
- ( Marker "suc" ) NonAssoc
- )
- [ NamedVar "a" ]
- ( ReplacePred
- ( NamedVar "y" )
- ( NamedVar "x" )
- ( TermVar
- ( NamedVar "a" )
- )
- ( Scope
- ( TermSymbol
- ( Location
- { locFile = "test/examples/replace.tex"
- , locLine = 20
- , locColumn = 44
- }
- )
- ( SymbolPredicate
- ( PredicateRelation
- ( RelationSymbol
- ( Symbol "=" )
- ( ParameterArity 0 )
- ( Marker "eq" )
- )
- )
- )
- [ TermVar ( B ReplacementRangeVar )
- , TermSymbol
- ( Location
- { locFile = "test/examples/replace.tex"
- , locLine = 20
- , locColumn = 46
- }
- )
- ( SymbolMixfix
- ( MixfixItem
- ( TokenCons
- ( Command "cons" )
- ( TokenCons InvisibleBraceL
- ( HoleCons
- ( TokenCons InvisibleBraceR
- ( TokenCons InvisibleBraceL
- ( HoleCons ( TokenCons InvisibleBraceR End ) )
- )
- )
- )
- )
- )
- ( Marker "cons" ) NonAssoc
- )
- )
- [ TermVar ( B ReplacementDomVar )
- , TermSymbol
- ( Location
- { locFile = "test/examples/replace.tex"
- , locLine = 20
- , locColumn = 46
- }
- )
- ( SymbolMixfix
- ( MixfixItem
- ( TokenCons
- ( Command "emptyset" ) End
- )
- ( Marker "emptyset" ) NonAssoc
- )
- ) []
- ]
- ]
- )
- )
- )
- )
-, BlockLemma
- ( Location
- { locFile = "test/examples/replace.tex"
- , locLine = 25
- , locColumn = 1
- }
- )
- ( Marker "times_replacement_test" )
- ( Lemma []
- ( TermSymbol
- ( Location
- { locFile = "test/examples/replace.tex"
- , locLine = 26
- , locColumn = 16
- }
- )
- ( SymbolPredicate
- ( PredicateRelation
- ( RelationSymbol
- ( Symbol "=" )
- ( ParameterArity 0 )
- ( Marker "eq" )
- )
- )
- )
- [ TermSymbol
- ( Location
- { locFile = "test/examples/replace.tex"
- , locLine = 26
- , locColumn = 6
- }
- )
- ( SymbolMixfix
- ( MixfixItem
- ( HoleCons
- ( TokenCons
- ( Command "times" ) ( HoleCons End )
- )
- )
- ( Marker "times" ) RightAssoc
- )
- )
- [ TermVar
- ( NamedVar "A" )
- , TermVar
- ( NamedVar "B" )
- ]
- , ReplaceFun
- (
- ( NamedVar "a"
- , TermVar
- ( NamedVar "A" )
- ) :|
- [
- ( NamedVar "b"
- , TermVar
- ( NamedVar "B" )
- )
- ]
- )
- ( Scope
- ( TermSymbol
- ( Location
- { locFile = "test/examples/replace.tex"
- , locLine = 26
- , locColumn = 21
- }
- )
- ( SymbolMixfix
- ( MixfixItem
- ( TokenCons
- ( Command "pair" )
- ( TokenCons InvisibleBraceL
- ( HoleCons
- ( TokenCons InvisibleBraceR
- ( TokenCons InvisibleBraceL
- ( HoleCons ( TokenCons InvisibleBraceR End ) )
- )
- )
- )
- )
- )
- ( Marker "pair" ) NonAssoc
- )
- )
- [ TermVar
- ( B
- ( NamedVar "a" )
- )
- , TermVar
- ( B
- ( NamedVar "b" )
- )
- ]
- )
- )
- ( Scope ( PropositionalConstant IsTop ) )
- ]
- )
- )
-] \ No newline at end of file
generated by cgit v1.2.3 (git 2.39.1) at 2026-08-04 10:44:15 +0000