| Safe Haskell | None |
|---|---|
| Language | Haskell2010 |
Agda.Utils.String
Synopsis
- quote :: String -> String
- haskellStringLiteral :: String -> String
- delimiter :: String -> String
- showIndex :: (Show i, Integral i) => i -> String
- addFinalNewLine :: String -> String
- indent :: Integral i => i -> String -> String
- newtype Str = Str {}
- showThousandSep :: Show a => a -> String
- ltrim :: String -> String
- rtrim :: String -> String
- trim :: String -> String
Documentation
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.)
haskellStringLiteral :: String -> String #
Turns the string into a Haskell string literal, avoiding escape codes.
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 unless the user explicitly asked us to not use any unicode characters.
addFinalNewLine :: String -> String #
Adds a final newline if there is not already one.
showThousandSep :: Show a => a -> String #
Show a number using comma to separate powers of 1,000.