aboutsummaryrefslogtreecommitdiffhomepage
path: root/lib/ur/basis.urs
diff options
context:
space:
mode:
authorGravatar Adam Chlipala <adamc@hcoop.net>2010-01-12 16:09:13 -0500
committerGravatar Adam Chlipala <adamc@hcoop.net>2010-01-12 16:09:13 -0500
commit227c87323603dc0b338e89997d2fce7ffc755fb0 (patch)
treee4130a31cf93875c66cb452ebcf893a4d2254f25 /lib/ur/basis.urs
parent8eab6ba5a16002cd6e5ddfb6a09cb23b351c9d32 (diff)
Allow escaped backslashes in literals; conversion betwixt int and char
Diffstat (limited to 'lib/ur/basis.urs')
-rw-r--r--lib/ur/basis.urs3
1 files changed, 2 insertions, 1 deletions
diff --git a/lib/ur/basis.urs b/lib/ur/basis.urs
index d61763af..ea50b0b3 100644
--- a/lib/ur/basis.urs
+++ b/lib/ur/basis.urs
@@ -68,7 +68,8 @@ val isupper : char -> bool
val isxdigit : char -> bool
val tolower : char -> char
val toupper : char -> char
-
+val ord : char -> int
+val chr : int -> char
(** String operations *)