aboutsummaryrefslogtreecommitdiffhomepage
path: root/lib/ur/basis.urs
diff options
context:
space:
mode:
authorGravatar Adam Chlipala <adam@chlipala.net>2011-01-13 10:02:50 -0500
committerGravatar Adam Chlipala <adam@chlipala.net>2011-01-13 10:02:50 -0500
commit24c29015ba668b044be7428f69058687a56d6a06 (patch)
treead413eedbc7c3eed30a276f339d9adf87ff01e49 /lib/ur/basis.urs
parent4eb2a196fa24d52462f3f325d73952fe2d1c12cd (diff)
More string processing
Diffstat (limited to 'lib/ur/basis.urs')
-rw-r--r--lib/ur/basis.urs1
1 files changed, 1 insertions, 0 deletions
diff --git a/lib/ur/basis.urs b/lib/ur/basis.urs
index 0b22544f..a91fd498 100644
--- a/lib/ur/basis.urs
+++ b/lib/ur/basis.urs
@@ -87,6 +87,7 @@ val strsub : string -> int -> char
val strsuffix : string -> int -> string
val strchr : string -> char -> option string
val strindex : string -> char -> option int
+val strsindex : string -> string -> option int
val strcspn : string -> string -> int
val substring : string -> int -> int -> string
val str1 : char -> string