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

Safe Haskell | Safe-Inferred
Language | Haskell2010

Agda.Utils.Char

Description

Agda strings uses Data.Text [1], which can only represent unicode scalar values [2], excluding the surrogate code points 3. To allow `primStringFromList` to be injective we make sure character values also exclude surrogate code points, mapping them to the replacement character `U+FFFD`.

See #4999 for more information.

1
  https://hackage.haskell.org/package/text-1.2.4.0/docs/Data-Text.html#g:2
2
  https://www.unicode.org/glossary/#unicode_scalar_value
3
  https://www.unicode.org/glossary/#surrogate_code_point

Synopsis

- replacementChar :: Char
- isSurrogateCodePoint :: Char -> Bool
- replaceSurrogateCodePoint :: Char -> Char
- integerToChar :: Integer -> Char

# Documentation

replacementChar :: Char Source #

The unicode replacement character � .

isSurrogateCodePoint :: Char -> Bool Source #

Is a character a surrogate code point.

replaceSurrogateCodePoint :: Char -> Char Source #

Map surrogate code points to the unicode replacement character.

integerToChar :: Integer -> Char Source #

Total function to convert an integer to a character. Maps surrogate code points to the replacement character `U+FFFD`.