test/golden/inductive/parsing.golden


1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84

[ BlockInductive
    ( Location
        { locFile = "test/examples/inductive.tex"
        , locLine = 3
        , locColumn = 1
        }
    ) Nothing
    ( Marker "fin" )
    ( Inductive
        { inductiveSymbolPattern = SymbolPattern
            ( MixfixItem
                ( TokenCons
                    ( Command "fin" )
                    ( TokenCons InvisibleBraceL
                        ( HoleCons ( TokenCons InvisibleBraceR End ) )
                    )
                )
                ( Marker "fin" ) NonAssoc
            )
            [ NamedVar "A" ]
        , inductiveDomain = ExprOp
            ( Location
                { locFile = "test/examples/inductive.tex"
                , locLine = 4
                , locColumn = 29
                }
            )
            ( MixfixItem
                ( TokenCons
                    ( Command "cumul" )
                    ( TokenCons InvisibleBraceL
                        ( HoleCons ( TokenCons InvisibleBraceR End ) )
                    )
                )
                ( Marker "cumul" ) NonAssoc
            )
            [ ExprVar
                ( NamedVar "A" )
            ]
        , inductiveIntros = IntroRule
            { introConditions = []
            , introResult = FormulaChain
                ( ChainBase
                    ( ExprVar
                        ( NamedVar "A" ) :| []
                    ) Positive
                    ( Relation
                        ( Location
                            { locFile = "test/examples/inductive.tex"
                            , locLine = 6
                            , locColumn = 17
                            }
                        )
                        ( RelationSymbol
                            ( Command "in" )
                            ( ParameterArity 0 )
                            ( Marker "elem" )
                        ) []
                    )
                    ( ExprOp
                        ( Location
                            { locFile = "test/examples/inductive.tex"
                            , locLine = 6
                            , locColumn = 20
                            }
                        )
                        ( MixfixItem
                            ( TokenCons
                                ( Command "fin" )
                                ( TokenCons InvisibleBraceL
                                    ( HoleCons ( TokenCons InvisibleBraceR End ) )
                                )
                            )
                            ( Marker "fin" ) NonAssoc
                        )
                        [ ExprVar
                            ( NamedVar "A" )
                        ] :| []
                    )
                )
            } :| []
        }
    )
]