summaryrefslogtreecommitdiff
path: root/test/golden/union/glossing.golden
diff options
context:
space:
mode:
Diffstat (limited to 'test/golden/union/glossing.golden')
-rw-r--r--test/golden/union/glossing.golden734
1 files changed, 0 insertions, 734 deletions
diff --git a/test/golden/union/glossing.golden b/test/golden/union/glossing.golden
deleted file mode 100644
index 31d05fe..0000000
--- a/test/golden/union/glossing.golden
+++ /dev/null
@@ -1,734 +0,0 @@
-[ BlockAxiom
- ( Location
- { locFile = "test/examples/union.tex"
- , locLine = 1
- , locColumn = 1
- }
- )
- ( Marker "ext" )
- ( Axiom
- [ Asm
- ( Quantified Universally
- ( Scope
- ( Connected Equivalence
- ( TermSymbol
- ( Location
- { locFile = "test/examples/union.tex"
- , locLine = 2
- , locColumn = 35
- }
- )
- ( SymbolPredicate
- ( PredicateRelation
- ( RelationSymbol
- ( Command "in" )
- ( ParameterArity 0 )
- ( Marker "elem" )
- )
- )
- )
- [ TermVar
- ( B
- ( NamedVar "a" )
- )
- , TermVar
- ( F
- ( TermVar
- ( NamedVar "A" )
- )
- )
- ]
- )
- ( TermSymbol
- ( Location
- { locFile = "test/examples/union.tex"
- , locLine = 2
- , locColumn = 48
- }
- )
- ( SymbolPredicate
- ( PredicateRelation
- ( RelationSymbol
- ( Command "in" )
- ( ParameterArity 0 )
- ( Marker "elem" )
- )
- )
- )
- [ TermVar
- ( B
- ( NamedVar "a" )
- )
- , TermVar
- ( F
- ( TermVar
- ( NamedVar "B" )
- )
- )
- ]
- )
- )
- )
- )
- ]
- ( TermSymbol
- ( Location
- { locFile = "test/examples/union.tex"
- , locLine = 3
- , locColumn = 13
- }
- )
- ( SymbolPredicate
- ( PredicateRelation
- ( RelationSymbol
- ( Symbol "=" )
- ( ParameterArity 0 )
- ( Marker "eq" )
- )
- )
- )
- [ TermVar
- ( NamedVar "A" )
- , TermVar
- ( NamedVar "B" )
- ]
- )
- )
-, BlockAxiom
- ( Location
- { locFile = "test/examples/union.tex"
- , locLine = 6
- , locColumn = 1
- }
- )
- ( Marker "union_defn" )
- ( Axiom
- [ Asm ( PropositionalConstant IsTop )
- , Asm ( PropositionalConstant IsTop )
- ]
- ( Connected Equivalence
- ( TermSymbol
- ( Location
- { locFile = "test/examples/union.tex"
- , locLine = 8
- , locColumn = 7
- }
- )
- ( SymbolPredicate
- ( PredicateRelation
- ( RelationSymbol
- ( Command "in" )
- ( ParameterArity 0 )
- ( Marker "elem" )
- )
- )
- )
- [ TermVar
- ( NamedVar "a" )
- , TermSymbol
- ( Location
- { locFile = "test/examples/union.tex"
- , locLine = 8
- , locColumn = 11
- }
- )
- ( SymbolMixfix
- ( MixfixItem
- ( HoleCons
- ( TokenCons
- ( Command "union" ) ( HoleCons End )
- )
- )
- ( Marker "union" ) LeftAssoc
- )
- )
- [ TermVar
- ( NamedVar "A" )
- , TermVar
- ( NamedVar "B" )
- ]
- ]
- )
- ( Connected Disjunction
- ( TermSymbol
- ( Location
- { locFile = "test/examples/union.tex"
- , locLine = 8
- , locColumn = 28
- }
- )
- ( SymbolPredicate
- ( PredicateRelation
- ( RelationSymbol
- ( Command "in" )
- ( ParameterArity 0 )
- ( Marker "elem" )
- )
- )
- )
- [ TermVar
- ( NamedVar "a" )
- , TermVar
- ( NamedVar "A" )
- ]
- )
- ( TermSymbol
- ( Location
- { locFile = "test/examples/union.tex"
- , locLine = 8
- , locColumn = 40
- }
- )
- ( SymbolPredicate
- ( PredicateRelation
- ( RelationSymbol
- ( Command "in" )
- ( ParameterArity 0 )
- ( Marker "elem" )
- )
- )
- )
- [ TermVar
- ( NamedVar "a" )
- , TermVar
- ( NamedVar "B" )
- ]
- )
- )
- )
- )
-, BlockLemma
- ( Location
- { locFile = "test/examples/union.tex"
- , locLine = 11
- , locColumn = 1
- }
- )
- ( Marker "union_comm" )
- ( Lemma []
- ( TermSymbol
- ( Location
- { locFile = "test/examples/union.tex"
- , locLine = 12
- , locColumn = 16
- }
- )
- ( SymbolPredicate
- ( PredicateRelation
- ( RelationSymbol
- ( Symbol "=" )
- ( ParameterArity 0 )
- ( Marker "eq" )
- )
- )
- )
- [ TermSymbol
- ( Location
- { locFile = "test/examples/union.tex"
- , locLine = 12
- , locColumn = 6
- }
- )
- ( SymbolMixfix
- ( MixfixItem
- ( HoleCons
- ( TokenCons
- ( Command "union" ) ( HoleCons End )
- )
- )
- ( Marker "union" ) LeftAssoc
- )
- )
- [ TermVar
- ( NamedVar "A" )
- , TermVar
- ( NamedVar "B" )
- ]
- , TermSymbol
- ( Location
- { locFile = "test/examples/union.tex"
- , locLine = 12
- , locColumn = 18
- }
- )
- ( SymbolMixfix
- ( MixfixItem
- ( HoleCons
- ( TokenCons
- ( Command "union" ) ( HoleCons End )
- )
- )
- ( Marker "union" ) LeftAssoc
- )
- )
- [ TermVar
- ( NamedVar "B" )
- , TermVar
- ( NamedVar "A" )
- ]
- ]
- )
- )
-, BlockLemma
- ( Location
- { locFile = "test/examples/union.tex"
- , locLine = 15
- , locColumn = 1
- }
- )
- ( Marker "union_assoc" )
- ( Lemma []
- ( TermSymbol
- ( Location
- { locFile = "test/examples/union.tex"
- , locLine = 16
- , locColumn = 26
- }
- )
- ( SymbolPredicate
- ( PredicateRelation
- ( RelationSymbol
- ( Symbol "=" )
- ( ParameterArity 0 )
- ( Marker "eq" )
- )
- )
- )
- [ TermSymbol
- ( Location
- { locFile = "test/examples/union.tex"
- , locLine = 16
- , locColumn = 7
- }
- )
- ( SymbolMixfix
- ( MixfixItem
- ( HoleCons
- ( TokenCons
- ( Command "union" ) ( HoleCons End )
- )
- )
- ( Marker "union" ) LeftAssoc
- )
- )
- [ TermSymbol
- ( Location
- { locFile = "test/examples/union.tex"
- , locLine = 16
- , locColumn = 7
- }
- )
- ( SymbolMixfix
- ( MixfixItem
- ( HoleCons
- ( TokenCons
- ( Command "union" ) ( HoleCons End )
- )
- )
- ( Marker "union" ) LeftAssoc
- )
- )
- [ TermVar
- ( NamedVar "A" )
- , TermVar
- ( NamedVar "B" )
- ]
- , TermVar
- ( NamedVar "C" )
- ]
- , TermSymbol
- ( Location
- { locFile = "test/examples/union.tex"
- , locLine = 16
- , locColumn = 28
- }
- )
- ( SymbolMixfix
- ( MixfixItem
- ( HoleCons
- ( TokenCons
- ( Command "union" ) ( HoleCons End )
- )
- )
- ( Marker "union" ) LeftAssoc
- )
- )
- [ TermVar
- ( NamedVar "A" )
- , TermSymbol
- ( Location
- { locFile = "test/examples/union.tex"
- , locLine = 16
- , locColumn = 37
- }
- )
- ( SymbolMixfix
- ( MixfixItem
- ( HoleCons
- ( TokenCons
- ( Command "union" ) ( HoleCons End )
- )
- )
- ( Marker "union" ) LeftAssoc
- )
- )
- [ TermVar
- ( NamedVar "B" )
- , TermVar
- ( NamedVar "C" )
- ]
- ]
- ]
- )
- )
-, BlockProof
- ( Location
- { locFile = "test/examples/union.tex"
- , locLine = 18
- , locColumn = 1
- }
- )
- ( Location
- { locFile = "test/examples/union.tex"
- , locLine = 21
- , locColumn = 1
- }
- )
- ( Have
- ( Location
- { locFile = "test/examples/union.tex"
- , locLine = 19
- , locColumn = 5
- }
- )
- ( Quantified Universally
- ( Scope
- ( Connected Implication
- ( TermSymbol
- ( Location
- { locFile = "test/examples/union.tex"
- , locLine = 19
- , locColumn = 30
- }
- )
- ( SymbolPredicate
- ( PredicateRelation
- ( RelationSymbol
- ( Command "in" )
- ( ParameterArity 0 )
- ( Marker "elem" )
- )
- )
- )
- [ TermVar
- ( B
- ( NamedVar "a" )
- )
- , TermSymbol
- ( Location
- { locFile = "test/examples/union.tex"
- , locLine = 19
- , locColumn = 35
- }
- )
- ( SymbolMixfix
- ( MixfixItem
- ( HoleCons
- ( TokenCons
- ( Command "union" ) ( HoleCons End )
- )
- )
- ( Marker "union" ) LeftAssoc
- )
- )
- [ TermSymbol
- ( Location
- { locFile = "test/examples/union.tex"
- , locLine = 19
- , locColumn = 35
- }
- )
- ( SymbolMixfix
- ( MixfixItem
- ( HoleCons
- ( TokenCons
- ( Command "union" ) ( HoleCons End )
- )
- )
- ( Marker "union" ) LeftAssoc
- )
- )
- [ TermVar
- ( F
- ( TermVar
- ( NamedVar "A" )
- )
- )
- , TermVar
- ( F
- ( TermVar
- ( NamedVar "B" )
- )
- )
- ]
- , TermVar
- ( F
- ( TermVar
- ( NamedVar "C" )
- )
- )
- ]
- ]
- )
- ( TermSymbol
- ( Location
- { locFile = "test/examples/union.tex"
- , locLine = 19
- , locColumn = 63
- }
- )
- ( SymbolPredicate
- ( PredicateRelation
- ( RelationSymbol
- ( Command "in" )
- ( ParameterArity 0 )
- ( Marker "elem" )
- )
- )
- )
- [ TermVar
- ( B
- ( NamedVar "a" )
- )
- , TermSymbol
- ( Location
- { locFile = "test/examples/union.tex"
- , locLine = 19
- , locColumn = 67
- }
- )
- ( SymbolMixfix
- ( MixfixItem
- ( HoleCons
- ( TokenCons
- ( Command "union" ) ( HoleCons End )
- )
- )
- ( Marker "union" ) LeftAssoc
- )
- )
- [ TermVar
- ( F
- ( TermVar
- ( NamedVar "A" )
- )
- )
- , TermSymbol
- ( Location
- { locFile = "test/examples/union.tex"
- , locLine = 19
- , locColumn = 76
- }
- )
- ( SymbolMixfix
- ( MixfixItem
- ( HoleCons
- ( TokenCons
- ( Command "union" ) ( HoleCons End )
- )
- )
- ( Marker "union" ) LeftAssoc
- )
- )
- [ TermVar
- ( F
- ( TermVar
- ( NamedVar "B" )
- )
- )
- , TermVar
- ( F
- ( TermVar
- ( NamedVar "C" )
- )
- )
- ]
- ]
- ]
- )
- )
- )
- ) JustificationEmpty
- ( Have
- ( Location
- { locFile = "test/examples/union.tex"
- , locLine = 20
- , locColumn = 5
- }
- )
- ( Quantified Universally
- ( Scope
- ( Connected Implication
- ( TermSymbol
- ( Location
- { locFile = "test/examples/union.tex"
- , locLine = 20
- , locColumn = 30
- }
- )
- ( SymbolPredicate
- ( PredicateRelation
- ( RelationSymbol
- ( Command "in" )
- ( ParameterArity 0 )
- ( Marker "elem" )
- )
- )
- )
- [ TermVar
- ( B
- ( NamedVar "a" )
- )
- , TermSymbol
- ( Location
- { locFile = "test/examples/union.tex"
- , locLine = 20
- , locColumn = 34
- }
- )
- ( SymbolMixfix
- ( MixfixItem
- ( HoleCons
- ( TokenCons
- ( Command "union" ) ( HoleCons End )
- )
- )
- ( Marker "union" ) LeftAssoc
- )
- )
- [ TermVar
- ( F
- ( TermVar
- ( NamedVar "A" )
- )
- )
- , TermSymbol
- ( Location
- { locFile = "test/examples/union.tex"
- , locLine = 20
- , locColumn = 43
- }
- )
- ( SymbolMixfix
- ( MixfixItem
- ( HoleCons
- ( TokenCons
- ( Command "union" ) ( HoleCons End )
- )
- )
- ( Marker "union" ) LeftAssoc
- )
- )
- [ TermVar
- ( F
- ( TermVar
- ( NamedVar "B" )
- )
- )
- , TermVar
- ( F
- ( TermVar
- ( NamedVar "C" )
- )
- )
- ]
- ]
- ]
- )
- ( TermSymbol
- ( Location
- { locFile = "test/examples/union.tex"
- , locLine = 20
- , locColumn = 63
- }
- )
- ( SymbolPredicate
- ( PredicateRelation
- ( RelationSymbol
- ( Command "in" )
- ( ParameterArity 0 )
- ( Marker "elem" )
- )
- )
- )
- [ TermVar
- ( B
- ( NamedVar "a" )
- )
- , TermSymbol
- ( Location
- { locFile = "test/examples/union.tex"
- , locLine = 20
- , locColumn = 68
- }
- )
- ( SymbolMixfix
- ( MixfixItem
- ( HoleCons
- ( TokenCons
- ( Command "union" ) ( HoleCons End )
- )
- )
- ( Marker "union" ) LeftAssoc
- )
- )
- [ TermSymbol
- ( Location
- { locFile = "test/examples/union.tex"
- , locLine = 20
- , locColumn = 68
- }
- )
- ( SymbolMixfix
- ( MixfixItem
- ( HoleCons
- ( TokenCons
- ( Command "union" ) ( HoleCons End )
- )
- )
- ( Marker "union" ) LeftAssoc
- )
- )
- [ TermVar
- ( F
- ( TermVar
- ( NamedVar "A" )
- )
- )
- , TermVar
- ( F
- ( TermVar
- ( NamedVar "B" )
- )
- )
- ]
- , TermVar
- ( F
- ( TermVar
- ( NamedVar "C" )
- )
- )
- ]
- ]
- )
- )
- )
- ) JustificationEmpty
- ( Qed
- { mloc = Nothing
- , by = JustificationEmpty
- }
- )
- )
- )
-] \ No newline at end of file
generated by cgit v1.2.3 (git 2.39.1) at 2026-08-04 14:09:57 +0000