Agda.Utils.String

Documentation

quote :: String -> String

quote adds double quotes around the string, replaces newline characters with n, and escapes double quotes and backslashes within the string. This is different from the behaviour of show:

> putStrLn $ show "\x2200"
"\8704"
> putStrLn $ quote "\x2200"
"∀"

(The code examples above have been tested using version 4.2.0.0 of the base library.)

delimiter :: String -> String

Adds hyphens around the given string

>>> putStrLn $ delimiter "Title"
———— Title —————————————————————————————————————————————————

showIndex :: (Show i, Integral i) => i -> String

Shows a non-negative integer using the characters ₀-₉ instead of 0-9.

addFinalNewLine :: String -> String

Adds a final newline if there is not already one.

indent :: Integral i => i -> String -> String

Indents every line the given number of steps.

newtype Str

Constructors

Str

Fields

• unStr :: String

Instances

Eq Str

Methods

(==) :: Str -> Str -> Bool

(/=) :: Str -> Str -> Bool

Show Str

Methods

showsPrec :: Int -> Str -> ShowS

show :: Str -> String

showList :: [Str] -> ShowS

FromTerm Str

Methods

fromTerm :: TCM (FromTermFunction Str)

ToTerm Str

Methods

toTerm :: TCM (Str -> Term)

toTermR :: TCM (Str -> ReduceM Term)

PrimTerm Str

Methods

primTerm :: Str -> TCM Term

Unquote Str

Methods

unquote :: Term -> UnquoteM Str

showThousandSep :: Show a => a -> String

Show a number using comma to separate powers of 1,000.

ltrim :: String -> String

Remove leading whitespace.

rtrim :: String -> String

Remove trailing whitespace.

trim :: String -> String

Remove leading and trailing whitesapce.