Prelude.Show

Definitions

data Prec : Type

  The precedence of an Idris operator or syntactic context.

Totality: total
Visibility: public export
Constructors:

Open : Prec
Equal : Prec
Dollar : Prec
Backtick : Prec
User : Nat -> Prec
PrefixMinus : Prec
App : Prec

Hints:

Eq Prec
Ord Prec

precCon : Prec -> Integer

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

Totality: total
Visibility: public export

interface Show : Type -> Type

  Things that have a canonical `String` representation.
  A minimal implementation includes either `show` or `showPrec`.

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)
Show Ordering

show : Show ty => ty -> String

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

Totality: total
Visibility: public export

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
Visibility: public export

showParens : Bool -> String -> String

  Surround a `String` with parentheses depending on a condition.
  @ b whether to add parentheses

Totality: total
Visibility: export

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:
  ```idris 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
Visibility: export

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
Visibility: export