Prelude.Show

data 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

interface Show : 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:

Show Int
Show Integer
Show Bits8
Show Bits16
Show Bits32
Show Bits64
Show Int8
Show Int16
Show Int32
Show Int64
Show Double
Show Char
Show String
Show Nat
Show Bool
Show Void
Show ()
(Show a, Show b) => Show (a, b)
(Show a, Show (p y)) => Show (DPair a p)
Show a => Show (List a)
Show a => Show (Maybe a)
(Show a, Show b) => Show (Either a b)

precCon : Prec -> Integer

  Gives the constructor index of the Prec as a helper for writing
  implementations.

Totality: total

show : Show ty => ty -> String

  Convert a value to its `String` representation.
  @ x the value to convert

Totality: total

showArg : Show a => 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 : Show ty => 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