diff options
Diffstat (limited to 'source/Syntax/Abstract.hs')
| -rw-r--r-- | source/Syntax/Abstract.hs | 15 |
1 files changed, 14 insertions, 1 deletions
diff --git a/source/Syntax/Abstract.hs b/source/Syntax/Abstract.hs index f589283..76ce6b6 100644 --- a/source/Syntax/Abstract.hs +++ b/source/Syntax/Abstract.hs @@ -168,7 +168,9 @@ pattern NeqSymbol = pattern SubseteqSymbol = RelationSymbol (Command "subseteq") (ParameterArity 0) "subseteq" --- | The predefined @cons@ function symbol used for desugaring finite set expressions. +-- | The ordinary source-level @cons@ function symbol. +-- +-- Finite-set notation is intrinsic and does not desugar through this symbol. pattern ConsSymbol :: FunctionSymbol pattern ConsSymbol = MixfixItem @@ -220,6 +222,17 @@ pattern UpairSymbol = "upair" NonAssoc +-- | The fixed family-union function symbol. +pattern UnionsSymbol :: FunctionSymbol +pattern UnionsSymbol = + MixfixItem + (TokenCons (Command "unions") + (TokenCons InvisibleBraceL + (HoleCons + (TokenCons InvisibleBraceR End)))) + "unions" + NonAssoc + -- | Function application /@f(x)@/ desugars to /@\apply{f}{x}@/. pattern ApplySymbol :: FunctionSymbol pattern ApplySymbol = |