summaryrefslogtreecommitdiff
path: root/test/golden/union
diff options
context:
space:
mode:
Diffstat (limited to 'test/golden/union')
-rw-r--r--test/golden/union/parsing.golden123
-rw-r--r--test/golden/union/scanning.golden9
-rw-r--r--test/golden/union/tokenizing.golden14
3 files changed, 104 insertions, 42 deletions
diff --git a/test/golden/union/parsing.golden b/test/golden/union/parsing.golden
index 4225bd8..df6361e 100644
--- a/test/golden/union/parsing.golden
+++ b/test/golden/union/parsing.golden
@@ -1,9 +1,50 @@
-[ BlockAxiom
+[ BlockSig
( Location
{ locFile = "test/examples/union.tex"
, locLine = 1
, locColumn = 1
}
+ ) Nothing
+ ( Marker "example_union" ) []
+ ( SignatureSymbolic
+ ( SymbolPattern
+ ( MixfixItem
+ ( HoleCons
+ ( TokenCons
+ ( Command "union" ) ( HoleCons End )
+ )
+ )
+ ( Marker "union" ) LeftAssoc
+ )
+ [ NamedVar "A"
+ , NamedVar "B"
+ ]
+ ) NounPhrase ( [] )
+ ( Noun
+ ( Location
+ { locFile = "test/examples/union.tex"
+ , locLine = 2
+ , locColumn = 22
+ }
+ )
+ ( LexicalItemSgPl
+ ( SgPl
+ { sg = TokenCons
+ ( Word "set" ) End
+ , pl = TokenCons
+ ( Word "sets" ) End
+ }
+ )
+ ( Marker "set" )
+ ) []
+ ) ( Nothing ) ( [] ) ( Nothing )
+ )
+, BlockAxiom
+ ( Location
+ { locFile = "test/examples/union.tex"
+ , locLine = 5
+ , locColumn = 1
+ }
)
( Just
[ Word "extensionality" ]
@@ -14,7 +55,7 @@
( SymbolicQuantified
{ loc = Location
{ locFile = "test/examples/union.tex"
- , locLine = 2
+ , locLine = 6
, locColumn = 13
}
, quant = Universally
@@ -33,7 +74,7 @@
( Relation
( Location
{ locFile = "test/examples/union.tex"
- , locLine = 2
+ , locLine = 6
, locColumn = 35
}
)
@@ -57,7 +98,7 @@
( Relation
( Location
{ locFile = "test/examples/union.tex"
- , locLine = 2
+ , locLine = 6
, locColumn = 48
}
)
@@ -85,7 +126,7 @@
( Relation
( Location
{ locFile = "test/examples/union.tex"
- , locLine = 3
+ , locLine = 7
, locColumn = 13
}
)
@@ -105,7 +146,7 @@
, BlockAxiom
( Location
{ locFile = "test/examples/union.tex"
- , locLine = 6
+ , locLine = 10
, locColumn = 1
}
) Nothing
@@ -118,7 +159,7 @@
( Noun
( Location
{ locFile = "test/examples/union.tex"
- , locLine = 7
+ , locLine = 11
, locColumn = 19
}
)
@@ -146,7 +187,7 @@
( Relation
( Location
{ locFile = "test/examples/union.tex"
- , locLine = 8
+ , locLine = 12
, locColumn = 7
}
)
@@ -159,7 +200,7 @@
( ExprOp
( Location
{ locFile = "test/examples/union.tex"
- , locLine = 8
+ , locLine = 12
, locColumn = 11
}
)
@@ -191,7 +232,7 @@
( Relation
( Location
{ locFile = "test/examples/union.tex"
- , locLine = 8
+ , locLine = 12
, locColumn = 28
}
)
@@ -215,7 +256,7 @@
( Relation
( Location
{ locFile = "test/examples/union.tex"
- , locLine = 8
+ , locLine = 12
, locColumn = 40
}
)
@@ -237,7 +278,7 @@
, BlockClaim Proposition
( Location
{ locFile = "test/examples/union.tex"
- , locLine = 11
+ , locLine = 15
, locColumn = 1
}
) Nothing
@@ -249,7 +290,7 @@
( ExprOp
( Location
{ locFile = "test/examples/union.tex"
- , locLine = 12
+ , locLine = 16
, locColumn = 6
}
)
@@ -270,7 +311,7 @@
( Relation
( Location
{ locFile = "test/examples/union.tex"
- , locLine = 12
+ , locLine = 16
, locColumn = 16
}
)
@@ -283,7 +324,7 @@
( ExprOp
( Location
{ locFile = "test/examples/union.tex"
- , locLine = 12
+ , locLine = 16
, locColumn = 18
}
)
@@ -308,7 +349,7 @@
, BlockClaim Proposition
( Location
{ locFile = "test/examples/union.tex"
- , locLine = 15
+ , locLine = 19
, locColumn = 1
}
) Nothing
@@ -320,7 +361,7 @@
( ExprOp
( Location
{ locFile = "test/examples/union.tex"
- , locLine = 16
+ , locLine = 20
, locColumn = 7
}
)
@@ -335,7 +376,7 @@
[ ExprOp
( Location
{ locFile = "test/examples/union.tex"
- , locLine = 16
+ , locLine = 20
, locColumn = 7
}
)
@@ -359,7 +400,7 @@
( Relation
( Location
{ locFile = "test/examples/union.tex"
- , locLine = 16
+ , locLine = 20
, locColumn = 26
}
)
@@ -372,7 +413,7 @@
( ExprOp
( Location
{ locFile = "test/examples/union.tex"
- , locLine = 16
+ , locLine = 20
, locColumn = 28
}
)
@@ -389,7 +430,7 @@
, ExprOp
( Location
{ locFile = "test/examples/union.tex"
- , locLine = 16
+ , locLine = 20
, locColumn = 37
}
)
@@ -415,21 +456,21 @@
, BlockProof
( Location
{ locFile = "test/examples/union.tex"
- , locLine = 18
+ , locLine = 22
, locColumn = 1
}
)
( Have
( Location
{ locFile = "test/examples/union.tex"
- , locLine = 19
+ , locLine = 23
, locColumn = 5
}
) Nothing
( SymbolicQuantified
{ loc = Location
{ locFile = "test/examples/union.tex"
- , locLine = 19
+ , locLine = 23
, locColumn = 5
}
, quant = Universally
@@ -441,7 +482,7 @@
, mloc = Just
( Location
{ locFile = "test/examples/union.tex"
- , locLine = 19
+ , locLine = 23
, locColumn = 25
}
)
@@ -454,7 +495,7 @@
( Relation
( Location
{ locFile = "test/examples/union.tex"
- , locLine = 19
+ , locLine = 23
, locColumn = 30
}
)
@@ -467,7 +508,7 @@
( ExprOp
( Location
{ locFile = "test/examples/union.tex"
- , locLine = 19
+ , locLine = 23
, locColumn = 35
}
)
@@ -482,7 +523,7 @@
[ ExprOp
( Location
{ locFile = "test/examples/union.tex"
- , locLine = 19
+ , locLine = 23
, locColumn = 35
}
)
@@ -514,7 +555,7 @@
( Relation
( Location
{ locFile = "test/examples/union.tex"
- , locLine = 19
+ , locLine = 23
, locColumn = 63
}
)
@@ -527,7 +568,7 @@
( ExprOp
( Location
{ locFile = "test/examples/union.tex"
- , locLine = 19
+ , locLine = 23
, locColumn = 67
}
)
@@ -544,7 +585,7 @@
, ExprOp
( Location
{ locFile = "test/examples/union.tex"
- , locLine = 19
+ , locLine = 23
, locColumn = 76
}
)
@@ -571,14 +612,14 @@
( Have
( Location
{ locFile = "test/examples/union.tex"
- , locLine = 20
+ , locLine = 24
, locColumn = 5
}
) Nothing
( SymbolicQuantified
{ loc = Location
{ locFile = "test/examples/union.tex"
- , locLine = 20
+ , locLine = 24
, locColumn = 5
}
, quant = Universally
@@ -590,7 +631,7 @@
, mloc = Just
( Location
{ locFile = "test/examples/union.tex"
- , locLine = 20
+ , locLine = 24
, locColumn = 25
}
)
@@ -603,7 +644,7 @@
( Relation
( Location
{ locFile = "test/examples/union.tex"
- , locLine = 20
+ , locLine = 24
, locColumn = 30
}
)
@@ -616,7 +657,7 @@
( ExprOp
( Location
{ locFile = "test/examples/union.tex"
- , locLine = 20
+ , locLine = 24
, locColumn = 34
}
)
@@ -633,7 +674,7 @@
, ExprOp
( Location
{ locFile = "test/examples/union.tex"
- , locLine = 20
+ , locLine = 24
, locColumn = 43
}
)
@@ -663,7 +704,7 @@
( Relation
( Location
{ locFile = "test/examples/union.tex"
- , locLine = 20
+ , locLine = 24
, locColumn = 63
}
)
@@ -676,7 +717,7 @@
( ExprOp
( Location
{ locFile = "test/examples/union.tex"
- , locLine = 20
+ , locLine = 24
, locColumn = 68
}
)
@@ -691,7 +732,7 @@
[ ExprOp
( Location
{ locFile = "test/examples/union.tex"
- , locLine = 20
+ , locLine = 24
, locColumn = 68
}
)
@@ -721,7 +762,7 @@
)
( Location
{ locFile = "test/examples/union.tex"
- , locLine = 21
+ , locLine = 25
, locColumn = 1
}
)
diff --git a/test/golden/union/scanning.golden b/test/golden/union/scanning.golden
index 0637a08..410ced6 100644
--- a/test/golden/union/scanning.golden
+++ b/test/golden/union/scanning.golden
@@ -1 +1,8 @@
-[] \ No newline at end of file
+[ ScanFunctionSymbol
+ ( HoleCons
+ ( TokenCons
+ ( Command "union" ) ( HoleCons End )
+ )
+ )
+ ( Marker "example_union" )
+] \ No newline at end of file
diff --git a/test/golden/union/tokenizing.golden b/test/golden/union/tokenizing.golden
index 1672765..37ce74e 100644
--- a/test/golden/union/tokenizing.golden
+++ b/test/golden/union/tokenizing.golden
@@ -1,4 +1,18 @@
[
+ [ BeginEnv "signature"
+ , Label "example_union"
+ , BeginEnv "math"
+ , Variable "A"
+ , Command "union"
+ , Variable "B"
+ , EndEnv "math"
+ , Word "is"
+ , Word "a"
+ , Word "set"
+ , Symbol "."
+ , EndEnv "signature"
+ ]
+,
[ BeginEnv "axiom"
, BracketL
, Word "extensionality"
generated by cgit v1.2.3 (git 2.39.1) at 2026-08-06 19:25:21 +0000