Idris2Doc : Prelude.Show

Prelude.Show

dataPrec : 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
interfaceShow : Type -> Type
  Things that have a canonical `String` representation.

Parameters: ty
Constructor: MkShow
Methods:
show : ty -> String
  Convert a value to its `String` representation.
@ x the value to convert
showPrec : 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

Implementations:
ShowInt
ShowInteger
ShowBits8
ShowBits16
ShowBits32
ShowBits64
ShowInt8
ShowInt16
ShowInt32
ShowInt64
ShowDouble
ShowChar
ShowString
ShowNat
ShowBool
ShowVoid
Show ()
(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