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

Safe Haskell | Safe-Inferred
Language | Haskell2010

Agda.Utils.Suffix

Synopsis

- isSubscriptDigit :: Char -> Bool
- toSubscriptDigit :: Char -> Char
- fromSubscriptDigit :: Char -> Char
- data Suffix
  - = Prime Integer
  - | Index Integer
  - | Subscript Integer
- nextSuffix :: Suffix -> Suffix
- suffixView :: String -> (String, Maybe Suffix)
- renderSuffix :: Suffix -> String
- addSuffix :: String -> Suffix -> String

# 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

Prime Integer | Identifier ends in `Integer` many primes.
Index Integer | Identifier ends in number `Integer` (ordinary digits).
Subscript Integer | Identifier ends in number `Integer` (subscript digits).

nextSuffix :: Suffix -> Suffix Source #

Increase the suffix by one.

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

Parse suffix.

renderSuffix :: Suffix -> String Source #

Print suffix.

addSuffix :: String -> Suffix -> String Source #