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

Safe HaskellSafe-Inferred

Agda.Utils.Suffix

Synopsis

Documentation

isSubscriptDigit :: Char -> BoolSource

Is the character one of the subscripts '@-@'?

toSubscriptDigit :: Char -> CharSource

Converts '0'@-@'9' to '@-@'.

Precondition: The digit needs to be in range.

fromSubscriptDigit :: Char -> CharSource

Converts '@-@' to '0'@-@'9'.

Precondition: The digit needs to be in range.