From d8801e05ef2f81f21eb27555b626ee2e52c3365f Mon Sep 17 00:00:00 2001 From: Adam Chlipala Date: Tue, 26 May 2009 12:25:06 -0400 Subject: Chars and more string operations --- lib/ur/string.ur | 4 ++++ 1 file changed, 4 insertions(+) create mode 100644 lib/ur/string.ur (limited to 'lib/ur/string.ur') diff --git a/lib/ur/string.ur b/lib/ur/string.ur new file mode 100644 index 00000000..5362805b --- /dev/null +++ b/lib/ur/string.ur @@ -0,0 +1,4 @@ +type t = Basis.string + +val sub = Basis.strsub +val suffix = Basis.strsuffix -- cgit v1.2.3