ilyakooo0/Idris-dev
1
0
Fork 0
mirror of https://github.com/ilyakooo0/Idris-dev.git synced 2024-11-11 14:57:30 +03:00
Code Issues Projects Releases Wiki Activity

Fix Char-Ascii docs

Browse Source
This commit is contained in:
Ilan Godik 2015-09-20 00:45:09 +03:00
parent aba225c3f5
commit 56afb44034
1 changed files with 2 additions and 2 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

4
libs/prelude/Prelude/Chars.idr
View File

@ -7,7 +7,7 @@ import Prelude.List
import Prelude.Cast
import Builtins
||| Return the ASCII representation of the character.
||| Convert the number to its ASCII equivalent.
chr : Int -> Char
chr x = if (x >= 0 && x < 0x110000)
then assert_total (prim__intToChar x)
@ -16,7 +16,7 @@ chr x = if (x >= 0 && x < 0x110000)
instance Cast Int Char where
cast = chr
||| Convert the number to its ASCII equivalent.
||| Return the ASCII representation of the character.
ord : Char -> Int
ord x = prim__charToInt x