diff options
Diffstat (limited to 'test/golden/finite-set-terms/glossing.golden')
| -rw-r--r-- | test/golden/finite-set-terms/glossing.golden | 238 |
1 files changed, 0 insertions, 238 deletions
diff --git a/test/golden/finite-set-terms/glossing.golden b/test/golden/finite-set-terms/glossing.golden deleted file mode 100644 index a531e00..0000000 --- a/test/golden/finite-set-terms/glossing.golden +++ /dev/null @@ -1,238 +0,0 @@ -[ BlockAxiom - ( Location - { locFile = "test/examples/finite-set-terms.tex" - , locLine = 1 - , locColumn = 1 - } - ) - ( Marker "cons" ) - ( Axiom [] - ( Connected Equivalence - ( TermSymbol - ( Location - { locFile = "test/examples/finite-set-terms.tex" - , locLine = 2 - , locColumn = 7 - } - ) - ( SymbolPredicate - ( PredicateRelation - ( RelationSymbol - ( Command "in" ) - ( ParameterArity 0 ) - ( Marker "elem" ) - ) - ) - ) - [ TermVar - ( NamedVar "x" ) - , TermSymbol - ( Location - { locFile = "test/examples/finite-set-terms.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/finite-set-terms.tex" - , locLine = 2 - , locColumn = 31 - } - ) - ( SymbolPredicate - ( PredicateRelation - ( RelationSymbol - ( Symbol "=" ) - ( ParameterArity 0 ) - ( Marker "eq" ) - ) - ) - ) - [ TermVar - ( NamedVar "x" ) - , TermVar - ( NamedVar "y" ) - ] - ) - ( TermSymbol - ( Location - { locFile = "test/examples/finite-set-terms.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/finite-set-terms.tex" - , locLine = 5 - , locColumn = 1 - } - ) - ( Marker "unit" ) - ( DefnOp - ( MixfixItem - ( TokenCons - ( Command "unit" ) End - ) - ( Marker "unit" ) NonAssoc - ) [] - ( TermSymbol - ( Location - { locFile = "test/examples/finite-set-terms.tex" - , locLine = 6 - , 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/finite-set-terms.tex" - , locLine = 6 - , locColumn = 16 - } - ) - ( SymbolMixfix - ( MixfixItem - ( TokenCons - ( Command "emptyset" ) End - ) - ( Marker "emptyset" ) NonAssoc - ) - ) [] - , TermSymbol - ( Location - { locFile = "test/examples/finite-set-terms.tex" - , locLine = 6 - , locColumn = 14 - } - ) - ( SymbolMixfix - ( MixfixItem - ( TokenCons - ( Command "emptyset" ) End - ) - ( Marker "emptyset" ) NonAssoc - ) - ) [] - ] - ) - ) -, BlockLemma - ( Location - { locFile = "test/examples/finite-set-terms.tex" - , locLine = 9 - , locColumn = 1 - } - ) - ( Marker "emptyset_in_unit" ) - ( Lemma [] - ( TermSymbol - ( Location - { locFile = "test/examples/finite-set-terms.tex" - , locLine = 10 - , locColumn = 15 - } - ) - ( SymbolPredicate - ( PredicateRelation - ( RelationSymbol - ( Command "in" ) - ( ParameterArity 0 ) - ( Marker "elem" ) - ) - ) - ) - [ TermSymbol - ( Location - { locFile = "test/examples/finite-set-terms.tex" - , locLine = 10 - , locColumn = 6 - } - ) - ( SymbolMixfix - ( MixfixItem - ( TokenCons - ( Command "emptyset" ) End - ) - ( Marker "emptyset" ) NonAssoc - ) - ) [] - , TermSymbol - ( Location - { locFile = "test/examples/finite-set-terms.tex" - , locLine = 10 - , locColumn = 18 - } - ) - ( SymbolMixfix - ( MixfixItem - ( TokenCons - ( Command "unit" ) End - ) - ( Marker "unit" ) NonAssoc - ) - ) [] - ] - ) - ) -]
\ No newline at end of file |