Skip to content

HORIZON HASKELL Docs lts/ghc-10.0.x77a86622026-10-31Search packagesCtrl K

Theme: |

GHC 10.0.0.20260917 · lts/ghc-10.0.x · 77a8662 · 2026-10-31

ModuleAgda-2.8.0.2Haskell2010

Agda.Utils.Char

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

value replacementChar
value isSurrogateCodePoint
value replaceSurrogateCodePoint
value integerToChar

PackageAgda-2.8.0.2
Exports4
LanguageHaskell2010
LicenceMIT
SourceChar.hs

valuereplacementChar :: Char

The unicode replacement character � .

valueisSurrogateCodePoint :: Char -> Bool

Is a character a surrogate code point.

valuereplaceSurrogateCodePoint :: Char -> Char

Map surrogate code points to the unicode replacement character.

valueintegerToChar :: Integer -> Char

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