@@ -9,7 +9,7 @@ import Builtins
10%access public export
10%access public export
12−||| Convert the number to its ASCII equivalent.
12+||| Convert the number to its Unicode equivalent.
13chr : Int -> Char
13chr : Int -> Char
14chr x = if (x >= 0 && x < 0x110000)
14chr x = if (x >= 0 && x < 0x110000)
15 then assert_total (prim__intToChar x)
15 then assert_total (prim__intToChar x)
@@ -18,7 +18,7 @@ chr x = if (x >= 0 && x < 0x110000)
18Cast Int Char where
18Cast Int Char where
19 cast = chr
19 cast = chr
21−||| Return the ASCII representation of the character.
21+||| Return the Unicode representation of the character.
22ord : Char -> Int
22ord : Char -> Int
23ord x = prim__charToInt x
23ord x = prim__charToInt x