summaryrefslogtreecommitdiff
path: root/lib
diff options
context:
space:
mode:
authorGravatar Adam Chlipala <adamc@hcoop.net>2008-09-07 12:15:46 -0400
committerGravatar Adam Chlipala <adamc@hcoop.net>2008-09-07 12:15:46 -0400
commit1f893091967ed6a9bd8469a62ddf4017e87d563d (patch)
tree5985b4036cf586410f210927f33ac86a4c6af0f9 /lib
parentf2829abe30366bc78ce8e5bd6272fac06a7f5b84 (diff)
Error-parsing ints
Diffstat (limited to 'lib')
-rw-r--r--lib/basis.urs2
1 files changed, 2 insertions, 0 deletions
diff --git a/lib/basis.urs b/lib/basis.urs
index b2f3122d..3bd2459c 100644
--- a/lib/basis.urs
+++ b/lib/basis.urs
@@ -32,6 +32,8 @@ val show_bool : show bool
class read
val read : t ::: Type -> read t -> string -> option t
+val readError : t ::: Type -> read t -> string -> t
+(* [readError] calls [error] if the input is malformed. *)
val read_int : read int
val read_float : read float
val read_string : read string