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

Safe HaskellSafe
LanguageHaskell98

Agda.Utils.Suffix

Synopsis

Documentation

isSubscriptDigit :: Char -> Bool Source

Is the character one of the subscripts '₀'-'₉'?

toSubscriptDigit :: Char -> Char Source

Converts '0'-'9' to '₀'-'₉'.

Precondition: The digit needs to be in range.

fromSubscriptDigit :: Char -> Char Source

Converts '₀'-'₉' to '0'-'9'.

Precondition: The digit needs to be in range.

data Suffix Source

Classification of identifier variants.

Constructors

NoSuffix 
Prime Int

Identifier ends in Int many primes.

Index Int

Identifier ends in number Int (ordinary digits).

Subscript Int

Identifier ends in number Int (subscript digits).

nextSuffix :: Suffix -> Suffix Source

Increase the suffix by one. If no suffix yet, put a subscript 1.

suffixView :: String -> (String, Suffix) Source

Parse suffix.

addSuffix :: String -> Suffix -> String Source

Print suffix.

nameVariant Source

Arguments

:: (String -> Bool)

Is the given name already taken?

-> String

Name of which we want an available variant.

-> String

Name extended by suffix that is not taken already.

Add first available Suffix to a name.