Agda-2.6.1.2: A dependently typed functional programming language and proof assistant
Safe HaskellNone
LanguageHaskell2010

Agda.Utils.String

Synopsis

Documentation

quote :: String -> String Source #

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 Source #

Turns the string into a Haskell string literal, avoiding escape codes.

delimiter :: String -> String Source #

Adds hyphens around the given string

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

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

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 Source #

Adds a final newline if there is not already one.

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

Indents every line the given number of steps.

newtype Str Source #

Constructors

Str 

Fields

Instances

Instances details
Eq Str Source # 
Instance details

Defined in Agda.Utils.String

Methods

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

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

Show Str Source # 
Instance details

Defined in Agda.Utils.String

Methods

showsPrec :: Int -> Str -> ShowS #

show :: Str -> String #

showList :: [Str] -> ShowS #

FromTerm Str Source # 
Instance details

Defined in Agda.TypeChecking.Primitive

ToTerm Str Source # 
Instance details

Defined in Agda.TypeChecking.Primitive

PrimTerm Str Source # 
Instance details

Defined in Agda.TypeChecking.Primitive

Methods

primTerm :: Str -> TCM Term Source #

Unquote Str Source # 
Instance details

Defined in Agda.TypeChecking.Unquote

showThousandSep :: Show a => a -> String Source #

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

ltrim :: String -> String Source #

Remove leading whitespace.

rtrim :: String -> String Source #

Remove trailing whitespace.

trim :: String -> String Source #

Remove leading and trailing whitesapce.

Orphan instances

(IsString (m a), Monad m) => IsString (ReaderT r m a) Source # 
Instance details

Methods

fromString :: String -> ReaderT r m a #

(IsString (m a), Monad m) => IsString (StateT s m a) Source # 
Instance details

Methods

fromString :: String -> StateT s m a #