Agda-2.4.2: A dependently typed functional programming language and proof assistant

Safe HaskellNone

Agda.Utils.String

Synopsis

Documentation

quote :: String -> StringSource

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.)

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

Shows a non-negative integer using the characters

addFinalNewLine :: String -> StringSource

Adds a final newline if there is not already one.

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

Indents every line the given number of steps.

newtype Str Source

Constructors

Str 

Fields

getStr :: String
 

Instances

Show Str 
Unquote Str 

showThousandSep :: Show a => a -> StringSource

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