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

Safe Haskell | Safe-Infered

Agda.Utils.Suffix

Synopsis

- 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

isSubscriptDigit :: Char -> Bool

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

toSubscriptDigit :: Char -> Char

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

Precondition: The digit needs to be in range.

fromSubscriptDigit :: Char -> Char

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

Precondition: The digit needs to be in range.

data Suffix

Constructors

NoSuffix |
Prime Int |
Index Int |
Subscript Int |

nextSuffix :: Suffix -> Suffix

suffixView :: String -> (String, Suffix)

addSuffix :: String -> Suffix -> String