blob: 132f408d083375820fc6574d00d220eb28566971 (
plain)
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
|
[ BlockLemma
( SourcePos
{ sourceName = "test/examples/separation.tex"
, sourceLine = Pos 1
, sourceColumn = Pos 1
}
)
( Marker "sep_test" )
( Lemma []
( StmtFormula
( FormulaChain
( ChainBase
( ExprVar
( NamedVar "X" ) :| []
) Positive
( RelationSymbol
( Symbol "=" )
) []
( ExprSep
( NamedVar "x" )
( ExprVar
( NamedVar "X" )
)
( StmtFormula
( FormulaChain
( ChainBase
( ExprVar
( NamedVar "x" ) :| []
) Positive
( RelationSymbol
( Symbol "=" )
) []
( ExprVar
( NamedVar "x" ) :| []
)
)
)
) :| []
)
)
)
)
)
]
|