Idris2Doc : Prelude.Show

Prelude.Show

Prec : Type
The precedence of an Idris operator or syntactic context.
Totality: total
Constructors:
Open : Prec
Equal : Prec
Dollar : Prec
Backtick : Prec
User : Nat -> Prec
PrefixMinus : Prec
App : Prec
Show : Type -> Type
Things that have a canonical `String` representation.
Parameters: ty
Methods:
show : (x : ty) -> String
Convert a value to its `String` representation.
@ x the value to convert
showPrec : (d : Prec) -> (x : ty) -> String
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`.
@ d the precedence context.
@ x the value to convert

Implementations:
Show Int
Show Integer
Show Bits8
Show Bits16
Show Bits32
Show Bits64
Show Double
Show Char
Show String
ShowNat
ShowBool
ShowUnit
(Showa, Showb) => Show (a, b)
(Showa, Show (py)) => Show (DPairap)
Showa => Show (Lista)
Showa => Show (Maybea)
(Showa, Showb) => Show (Eitherab)
precCon : Prec -> Integer
Gives the constructor index of the Prec as a helper for writing
implementations.
Totality: total
show : Showty => ty -> String
Convert a value to its `String` representation.
@ x the value to convert
Totality: total
showArg : Showa => a -> String
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.
Totality: total
showCon : Prec -> String -> String -> String
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
```
Totality: total
showParens : Bool -> String -> String
Surround a `String` with parentheses depending on a condition.
@ b whether to add parentheses
Totality: total
showPrec : Showty => Prec -> ty -> String
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`.
@ d the precedence context.
@ x the value to convert
Totality: total