summaryrefslogtreecommitdiff
path: root/test/golden/datatype/parsing.golden
diff options
context:
space:
mode:
Diffstat (limited to 'test/golden/datatype/parsing.golden')
-rw-r--r--test/golden/datatype/parsing.golden220
1 files changed, 176 insertions, 44 deletions
diff --git a/test/golden/datatype/parsing.golden b/test/golden/datatype/parsing.golden
index d07b92c..11dd2bc 100644
--- a/test/golden/datatype/parsing.golden
+++ b/test/golden/datatype/parsing.golden
@@ -88,15 +88,15 @@
, ExprFiniteSet
( Location
{ locFile = "test/examples/datatype.tex"
- , locLine = 6
- , locColumn = 54
+ , locLine = 7
+ , locColumn = 20
}
)
( ExprOp
( Location
{ locFile = "test/examples/datatype.tex"
- , locLine = 6
- , locColumn = 56
+ , locLine = 7
+ , locColumn = 22
}
)
( MixfixItem
@@ -113,7 +113,7 @@
{ datatypeClauseConstructorExpr = ExprOp
( Location
{ locFile = "test/examples/datatype.tex"
- , locLine = 7
+ , locLine = 8
, locColumn = 17
}
)
@@ -133,7 +133,7 @@
, datatypeClauseTargetExpr = ExprOp
( Location
{ locFile = "test/examples/datatype.tex"
- , locLine = 7
+ , locLine = 8
, locColumn = 34
}
)
@@ -149,7 +149,7 @@
, ExprOp
( Location
{ locFile = "test/examples/datatype.tex"
- , locLine = 7
+ , locLine = 8
, locColumn = 56
}
)
@@ -165,7 +165,7 @@
, ExprOp
( Location
{ locFile = "test/examples/datatype.tex"
- , locLine = 7
+ , locLine = 8
, locColumn = 78
}
)
@@ -184,7 +184,7 @@
, BlockClaim Proposition
( Location
{ locFile = "test/examples/datatype.tex"
- , locLine = 10
+ , locLine = 11
, locColumn = 1
}
) Nothing
@@ -196,7 +196,7 @@
( ExprOp
( Location
{ locFile = "test/examples/datatype.tex"
- , locLine = 11
+ , locLine = 12
, locColumn = 6
}
)
@@ -210,7 +210,7 @@
( Relation
( Location
{ locFile = "test/examples/datatype.tex"
- , locLine = 11
+ , locLine = 12
, locColumn = 15
}
)
@@ -223,7 +223,7 @@
( ExprOp
( Location
{ locFile = "test/examples/datatype.tex"
- , locLine = 11
+ , locLine = 12
, locColumn = 19
}
)
@@ -238,12 +238,38 @@
}
)
)
-, BlockClaim Proposition
+, BlockProof
( Location
{ locFile = "test/examples/datatype.tex"
, locLine = 14
, locColumn = 1
}
+ )
+ ( Qed
+ ( Just
+ ( Location
+ { locFile = "test/examples/datatype.tex"
+ , locLine = 15
+ , locColumn = 5
+ }
+ )
+ )
+ ( JustificationRef
+ ( Marker "propform_propbot_intro" :| [] )
+ )
+ )
+ ( Location
+ { locFile = "test/examples/datatype.tex"
+ , locLine = 16
+ , locColumn = 1
+ }
+ )
+, BlockClaim Proposition
+ ( Location
+ { locFile = "test/examples/datatype.tex"
+ , locLine = 18
+ , locColumn = 1
+ }
) Nothing
( Marker "propform_var_test" )
( Claim []
@@ -252,7 +278,7 @@
, mloc = Just
( Location
{ locFile = "test/examples/datatype.tex"
- , locLine = 15
+ , locLine = 19
, locColumn = 5
}
)
@@ -262,7 +288,7 @@
( ExprOp
( Location
{ locFile = "test/examples/datatype.tex"
- , locLine = 15
+ , locLine = 19
, locColumn = 9
}
)
@@ -276,7 +302,7 @@
( Relation
( Location
{ locFile = "test/examples/datatype.tex"
- , locLine = 15
+ , locLine = 19
, locColumn = 19
}
)
@@ -289,14 +315,14 @@
( ExprFiniteSet
( Location
{ locFile = "test/examples/datatype.tex"
- , locLine = 15
+ , locLine = 19
, locColumn = 23
}
)
( ExprOp
( Location
{ locFile = "test/examples/datatype.tex"
- , locLine = 15
+ , locLine = 19
, locColumn = 25
}
)
@@ -316,8 +342,8 @@
( ExprOp
( Location
{ locFile = "test/examples/datatype.tex"
- , locLine = 15
- , locColumn = 45
+ , locLine = 20
+ , locColumn = 10
}
)
( MixfixItem
@@ -332,8 +358,8 @@
[ ExprOp
( Location
{ locFile = "test/examples/datatype.tex"
- , locLine = 15
- , locColumn = 54
+ , locLine = 20
+ , locColumn = 19
}
)
( MixfixItem
@@ -347,8 +373,8 @@
( Relation
( Location
{ locFile = "test/examples/datatype.tex"
- , locLine = 15
- , locColumn = 65
+ , locLine = 20
+ , locColumn = 30
}
)
( RelationSymbol
@@ -360,8 +386,8 @@
( ExprOp
( Location
{ locFile = "test/examples/datatype.tex"
- , locLine = 15
- , locColumn = 69
+ , locLine = 20
+ , locColumn = 34
}
)
( MixfixItem
@@ -376,10 +402,36 @@
}
)
)
+, BlockProof
+ ( Location
+ { locFile = "test/examples/datatype.tex"
+ , locLine = 22
+ , locColumn = 1
+ }
+ )
+ ( Qed
+ ( Just
+ ( Location
+ { locFile = "test/examples/datatype.tex"
+ , locLine = 23
+ , locColumn = 5
+ }
+ )
+ )
+ ( JustificationRef
+ ( Marker "propform_propvar_intro" :| [] )
+ )
+ )
+ ( Location
+ { locFile = "test/examples/datatype.tex"
+ , locLine = 24
+ , locColumn = 1
+ }
+ )
, BlockClaim Proposition
( Location
{ locFile = "test/examples/datatype.tex"
- , locLine = 18
+ , locLine = 26
, locColumn = 1
}
) Nothing
@@ -391,7 +443,7 @@
( ExprOp
( Location
{ locFile = "test/examples/datatype.tex"
- , locLine = 19
+ , locLine = 27
, locColumn = 7
}
)
@@ -406,7 +458,7 @@
[ ExprOp
( Location
{ locFile = "test/examples/datatype.tex"
- , locLine = 19
+ , locLine = 27
, locColumn = 7
}
)
@@ -419,7 +471,7 @@
, ExprOp
( Location
{ locFile = "test/examples/datatype.tex"
- , locLine = 19
+ , locLine = 27
, locColumn = 24
}
)
@@ -434,7 +486,7 @@
( Relation
( Location
{ locFile = "test/examples/datatype.tex"
- , locLine = 19
+ , locLine = 27
, locColumn = 34
}
)
@@ -447,7 +499,7 @@
( ExprOp
( Location
{ locFile = "test/examples/datatype.tex"
- , locLine = 19
+ , locLine = 27
, locColumn = 38
}
)
@@ -462,10 +514,38 @@
}
)
)
+, BlockProof
+ ( Location
+ { locFile = "test/examples/datatype.tex"
+ , locLine = 29
+ , locColumn = 1
+ }
+ )
+ ( Qed
+ ( Just
+ ( Location
+ { locFile = "test/examples/datatype.tex"
+ , locLine = 30
+ , locColumn = 5
+ }
+ )
+ )
+ ( JustificationRef
+ ( Marker "propform_propbot_intro" :|
+ [ Marker "propform_propto_intro" ]
+ )
+ )
+ )
+ ( Location
+ { locFile = "test/examples/datatype.tex"
+ , locLine = 31
+ , locColumn = 1
+ }
+ )
, BlockClaim Proposition
( Location
{ locFile = "test/examples/datatype.tex"
- , locLine = 22
+ , locLine = 33
, locColumn = 1
}
) Nothing
@@ -477,7 +557,7 @@
( ExprOp
( Location
{ locFile = "test/examples/datatype.tex"
- , locLine = 23
+ , locLine = 34
, locColumn = 6
}
)
@@ -491,7 +571,7 @@
( Relation
( Location
{ locFile = "test/examples/datatype.tex"
- , locLine = 23
+ , locLine = 34
, locColumn = 15
}
)
@@ -504,7 +584,7 @@
( ExprOp
( Location
{ locFile = "test/examples/datatype.tex"
- , locLine = 23
+ , locLine = 34
, locColumn = 21
}
)
@@ -519,7 +599,7 @@
[ ExprOp
( Location
{ locFile = "test/examples/datatype.tex"
- , locLine = 23
+ , locLine = 34
, locColumn = 21
}
)
@@ -532,7 +612,7 @@
, ExprOp
( Location
{ locFile = "test/examples/datatype.tex"
- , locLine = 23
+ , locLine = 34
, locColumn = 38
}
)
@@ -548,10 +628,36 @@
}
)
)
+, BlockProof
+ ( Location
+ { locFile = "test/examples/datatype.tex"
+ , locLine = 36
+ , locColumn = 1
+ }
+ )
+ ( Qed
+ ( Just
+ ( Location
+ { locFile = "test/examples/datatype.tex"
+ , locLine = 37
+ , locColumn = 5
+ }
+ )
+ )
+ ( JustificationRef
+ ( Marker "propform_propbot_propto_distinct" :| [] )
+ )
+ )
+ ( Location
+ { locFile = "test/examples/datatype.tex"
+ , locLine = 38
+ , locColumn = 1
+ }
+ )
, BlockClaim Proposition
( Location
{ locFile = "test/examples/datatype.tex"
- , locLine = 26
+ , locLine = 40
, locColumn = 1
}
) Nothing
@@ -562,7 +668,7 @@
, mloc = Just
( Location
{ locFile = "test/examples/datatype.tex"
- , locLine = 27
+ , locLine = 41
, locColumn = 5
}
)
@@ -572,7 +678,7 @@
( ExprOp
( Location
{ locFile = "test/examples/datatype.tex"
- , locLine = 27
+ , locLine = 41
, locColumn = 9
}
)
@@ -592,7 +698,7 @@
( Relation
( Location
{ locFile = "test/examples/datatype.tex"
- , locLine = 27
+ , locLine = 41
, locColumn = 21
}
)
@@ -605,7 +711,7 @@
( ExprOp
( Location
{ locFile = "test/examples/datatype.tex"
- , locLine = 27
+ , locLine = 41
, locColumn = 23
}
)
@@ -633,7 +739,7 @@
( Relation
( Location
{ locFile = "test/examples/datatype.tex"
- , locLine = 27
+ , locLine = 41
, locColumn = 45
}
)
@@ -651,4 +757,30 @@
}
)
)
+, BlockProof
+ ( Location
+ { locFile = "test/examples/datatype.tex"
+ , locLine = 43
+ , locColumn = 1
+ }
+ )
+ ( Qed
+ ( Just
+ ( Location
+ { locFile = "test/examples/datatype.tex"
+ , locLine = 44
+ , locColumn = 5
+ }
+ )
+ )
+ ( JustificationRef
+ ( Marker "propform_propvar_injective" :| [] )
+ )
+ )
+ ( Location
+ { locFile = "test/examples/datatype.tex"
+ , locLine = 45
+ , locColumn = 1
+ }
+ )
] \ No newline at end of file
generated by cgit v1.2.3 (git 2.39.1) at 2026-08-06 18:46:52 +0000