The precedence of an Idris operator or syntactic context.
Things that have a canonical String
representation.
Convert a value to its String
representation.
Convert a value to its String
representation in a certain precedence
context.
A value should produce parentheses around itself if and only if the given
precedence context is greater than or equal to the precedence of the
outermost operation represented in the produced String
. This is
different from Haskell, which requires it to be strictly greater. Open
should thus always produce no outermost parens, App
should always
produce outermost parens except on atomic values and those that provide
their own bracketing, like Pair
and List
.
Gives the constructor index of the Prec as a helper for writing implementations.
A helper for the common case of showing a non-infix constructor with at
least one argument, for use with showCon
.
This adds a space to the front so the results can be directly
concatenated. See showCon
for details and an example.
A helper for the common case of showing a non-infix constructor with at
least one argument, for use with showArg
.
Apply showCon
to the precedence context, the constructor name, and the
args shown with showArg
and concatenated. Example:
data Ann a = MkAnn String a
Show a => Show (Ann a) where
showPrec d (MkAnn s x) = showCon d "MkAnn" $ showArg s ++ showArg x
Surround a String
with parentheses depending on a condition.
whether to add parentheses