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