Agda.Utils.String
Documentation
quote :: String -> StringSource
quote adds double quotes around the string, 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 :: Integral i => i -> StringSource
Shows a non-negative integer using the characters - instead of 0-9.
addFinalNewLine :: String -> StringSource
Adds a final newline if there is not already one.