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

Safe Haskell | None
Language | Haskell2010

Agda.Utils.Suffix

Synopsis

- subscriptAllowed :: UnicodeOrAscii
- isSubscriptDigit :: Char -> Bool
- toSubscriptDigit :: Char -> Char
- fromSubscriptDigit :: Char -> Char
- data Suffix
  - = NoSuffix
  - | Prime Int
  - | Index Int
  - | Subscript Int
- nextSuffix :: Suffix -> Suffix
- suffixView :: String -> (String, Suffix)
- addSuffix :: String -> Suffix -> String

# Documentation

subscriptAllowed :: UnicodeOrAscii Source #

Are we allowed to use unicode supscript characters?

isSubscriptDigit :: Char -> Bool Source #

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

toSubscriptDigit :: Char -> Char Source #

Converts `'0'`-`'9'` to `'₀'`-`'₉'` unless the user doesn't want us to use unicode characters

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.