diff options
| author | adelon <22380201+adelon@users.noreply.github.com> | 2025-08-12 00:37:28 +0200 |
|---|---|---|
| committer | adelon <22380201+adelon@users.noreply.github.com> | 2025-08-12 00:37:28 +0200 |
| commit | 39ef87d3ce39152febc130aa95e25dc0722c3525 (patch) | |
| tree | 018ce21f85bc132306ac5130db405527a313c1a7 /test/golden/inductive/parsing.golden | |
| parent | afce89ead823b6e9eec4a0b115bbe57a89a8e912 (diff) | |
Allow relation symbols with parameters
Parameters must follow the relation symbol and be surrounded by braces, like so: `\rel{x}{y}{z}`.
This attempt is still brittle/broken in a few ways:
- It makes using braces in creative ways in mixfix notation ambiguous.
- It does not verify that the parameters are used in a consistent manner for each symbol. It essentially allows users to define `a\MyRel b` and `a\MyRel{x} b` (and ones with even more parameters).
- It allows parameters for all relation symbols, even for those where it makes no sense in ordinary TeX markup, e.g. `a <{x} b`.
Diffstat (limited to 'test/golden/inductive/parsing.golden')
| -rw-r--r-- | test/golden/inductive/parsing.golden | 54 |
1 files changed, 27 insertions, 27 deletions
diff --git a/test/golden/inductive/parsing.golden b/test/golden/inductive/parsing.golden index 7438daa..6d5c0e3 100644 --- a/test/golden/inductive/parsing.golden +++ b/test/golden/inductive/parsing.golden @@ -9,7 +9,7 @@ ( Defn [] ( DefnRel ( NamedVar "A" ) - ( Command "subseteq" ) + ( Command "subseteq" ) [] ( NamedVar "B" ) ) ( StmtFormula @@ -20,7 +20,7 @@ ) Positive ( RelationSymbol ( Symbol "=" ) - ) + ) [] ( ExprVar ( NamedVar "B" ) :| [] ) @@ -176,7 +176,7 @@ ) Positive ( RelationSymbol ( Command "in" ) - ) + ) [] ( ExprOp [ Just ( Command "emptyset" ) @@ -224,7 +224,7 @@ ) Positive ( RelationSymbol ( Command "in" ) - ) + ) [] ( ExprOp [ Just ( Command "fin" ) @@ -247,7 +247,7 @@ ) Positive ( RelationSymbol ( Command "in" ) - ) + ) [] ( ExprVar ( NamedVar "A" ) :| [] ) @@ -259,7 +259,7 @@ ) Positive ( RelationSymbol ( Command "in" ) - ) + ) [] ( ExprOp [ Just ( Command "fin" ) @@ -293,7 +293,7 @@ ) Positive ( RelationSymbol ( Command "in" ) - ) + ) [] ( ExprOp [ Just ( Command "fin" ) @@ -345,7 +345,7 @@ ) Positive ( RelationSymbol ( Command "subseteq" ) - ) + ) [] ( ExprVar ( NamedVar "B" ) :| [] ) @@ -369,7 +369,7 @@ ) Positive ( RelationSymbol ( Command "subseteq" ) - ) + ) [] ( ExprOp [ Just ( Command "fin" ) @@ -438,7 +438,7 @@ ) Positive ( RelationSymbol ( Command "in" ) - ) + ) [] ( ExprVar ( NamedVar "R" ) :| [] ) @@ -451,7 +451,7 @@ ) Positive ( RelationSymbol ( Command "in" ) - ) + ) [] ( ExprOp [ Just ( Command "tracl" ) @@ -487,7 +487,7 @@ ) Positive ( RelationSymbol ( Command "in" ) - ) + ) [] ( ExprOp [ Just ( Command "tracl" ) @@ -520,7 +520,7 @@ ) Positive ( RelationSymbol ( Command "in" ) - ) + ) [] ( ExprVar ( NamedVar "R" ) :| [] ) @@ -546,7 +546,7 @@ ) Positive ( RelationSymbol ( Command "in" ) - ) + ) [] ( ExprOp [ Just ( Command "tracl" ) @@ -616,7 +616,7 @@ ) Positive ( RelationSymbol ( Command "in" ) - ) + ) [] ( ExprOp [ Just ( Command "fld" ) @@ -650,7 +650,7 @@ ) Positive ( RelationSymbol ( Command "in" ) - ) + ) [] ( ExprOp [ Just ( Command "qrefltracl" ) @@ -686,7 +686,7 @@ ) Positive ( RelationSymbol ( Command "in" ) - ) + ) [] ( ExprOp [ Just ( Command "qrefltracl" ) @@ -719,7 +719,7 @@ ) Positive ( RelationSymbol ( Command "in" ) - ) + ) [] ( ExprVar ( NamedVar "R" ) :| [] ) @@ -745,7 +745,7 @@ ) Positive ( RelationSymbol ( Command "in" ) - ) + ) [] ( ExprOp [ Just ( Command "qrefltracl" ) @@ -804,7 +804,7 @@ ) Positive ( RelationSymbol ( Command "in" ) - ) + ) [] ( ExprVar ( NamedVar "A" ) :| [] ) @@ -830,7 +830,7 @@ ) Positive ( RelationSymbol ( Command "in" ) - ) + ) [] ( ExprOp [ Just ( Command "refltracl" ) @@ -871,7 +871,7 @@ ) Positive ( RelationSymbol ( Command "in" ) - ) + ) [] ( ExprOp [ Just ( Command "refltracl" ) @@ -909,7 +909,7 @@ ) Positive ( RelationSymbol ( Command "in" ) - ) + ) [] ( ExprVar ( NamedVar "R" ) :| [] ) @@ -935,7 +935,7 @@ ) Positive ( RelationSymbol ( Command "in" ) - ) + ) [] ( ExprOp [ Just ( Command "refltracl" ) @@ -993,7 +993,7 @@ ) Positive ( RelationSymbol ( Command "in" ) - ) + ) [] ( ExprOp [ Just ( Command "fld" ) @@ -1028,7 +1028,7 @@ ) Positive ( RelationSymbol ( Command "in" ) - ) + ) [] ( ExprOp [ Just ( Command "pow" ) @@ -1057,7 +1057,7 @@ ) Positive ( RelationSymbol ( Command "in" ) - ) + ) [] ( ExprOp [ Just ( Command "acc" ) |