IdrisDoc: Prelude.Show

Prelude.Show

showParens : (b : Bool) -> String -> String

Surround a String with parentheses depending on a condition.

b

whether to add parentheses

showLitString : List Char -> String -> String
showLitChar : Char -> String -> String
showCon : (d : Prec) -> (conName : String) -> (shownArgs : 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
showArg : Show a => (x : 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.

protectEsc : (Char -> Bool) -> String -> String -> String
primNumShow : (a -> String) -> Prec -> a -> String
precCon : Prec -> Integer

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

firstCharIs : (Char -> Bool) -> String -> Bool
default#showPrec : Show ty => (d : Prec) -> (x : ty) -> String
default#show : Show ty => (x : ty) -> String
interface Show 

Things that have a canonical String representation.

show : Show ty => (x : ty) -> String

Convert a value to its String representation.

showPrec : Show ty => (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.

data Prec : Type

The precedence of an Idris operator or syntactic context.

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