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

Safe Haskell | Safe-Inferred

Agda.Utils.String

Synopsis

- quote :: String -> String
- showIndex :: (Show i, Integral i) => i -> String
- addFinalNewLine :: String -> String
- indent :: Integral i => i -> String -> 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.)

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

Shows a non-negative integer using the characters ₀-₉ instead o 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.