| Safe Haskell | None |
|---|---|
| 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.