summaryrefslogtreecommitdiff
path: root/test/golden/inductive/glossing.golden
diff options
context:
space:
mode:
Diffstat (limited to 'test/golden/inductive/glossing.golden')
-rw-r--r--test/golden/inductive/glossing.golden86
1 files changed, 0 insertions, 86 deletions
diff --git a/test/golden/inductive/glossing.golden b/test/golden/inductive/glossing.golden
deleted file mode 100644
index 98f60e8..0000000
--- a/test/golden/inductive/glossing.golden
+++ /dev/null
@@ -1,86 +0,0 @@
-[ BlockInductive
- ( Location
- { locFile = "test/examples/inductive.tex"
- , locLine = 3
- , locColumn = 1
- }
- )
- ( Marker "fin" )
- ( Inductive
- { inductiveSymbol = MixfixItem
- ( TokenCons
- ( Command "fin" )
- ( TokenCons InvisibleBraceL
- ( HoleCons ( TokenCons InvisibleBraceR End ) )
- )
- )
- ( Marker "fin" ) NonAssoc
- , inductiveParams =
- [ NamedVar "A" ]
- , inductiveDomain = TermSymbol
- ( Location
- { locFile = "test/examples/inductive.tex"
- , locLine = 4
- , locColumn = 29
- }
- )
- ( SymbolMixfix
- ( MixfixItem
- ( TokenCons
- ( Command "cumul" )
- ( TokenCons InvisibleBraceL
- ( HoleCons ( TokenCons InvisibleBraceR End ) )
- )
- )
- ( Marker "cumul" ) NonAssoc
- )
- )
- [ TermVar
- ( NamedVar "A" )
- ]
- , inductiveIntros = IntroRule
- { introConditions = []
- , introResult = TermSymbol
- ( Location
- { locFile = "test/examples/inductive.tex"
- , locLine = 6
- , locColumn = 17
- }
- )
- ( SymbolPredicate
- ( PredicateRelation
- ( RelationSymbol
- ( Command "in" )
- ( ParameterArity 0 )
- ( Marker "elem" )
- )
- )
- )
- [ TermVar
- ( NamedVar "A" )
- , TermSymbol
- ( Location
- { locFile = "test/examples/inductive.tex"
- , locLine = 6
- , locColumn = 20
- }
- )
- ( SymbolMixfix
- ( MixfixItem
- ( TokenCons
- ( Command "fin" )
- ( TokenCons InvisibleBraceL
- ( HoleCons ( TokenCons InvisibleBraceR End ) )
- )
- )
- ( Marker "fin" ) NonAssoc
- )
- )
- [ TermVar
- ( NamedVar "A" )
- ]
- ]
- } :| []
- }
- )
-] \ No newline at end of file