equal
deleted
inserted
replaced
7 structure String = |
7 structure String = |
8 struct |
8 struct |
9 fun isSuffix s1 s2 = |
9 fun isSuffix s1 s2 = |
10 let val n1 = size s1 and n2 = size s2 |
10 let val n1 = size s1 and n2 = size s2 |
11 in if n1 = n2 then s1 = s2 else n1 <= n2 andalso String.substring (s2, n2 - n1, n1) = s1 end; |
11 in if n1 = n2 then s1 = s2 else n1 <= n2 andalso String.substring (s2, n2 - n1, n1) = s1 end; |
|
12 fun isSubstring s1 s2 = |
|
13 String.isPrefix s1 s2 orelse |
|
14 size s1 < size s2 andalso isSubstring s1 (String.extract (s2, 1, NONE)); |
12 open String; |
15 open String; |
13 end; |
16 end; |
14 |
17 |
15 structure Substring = |
18 structure Substring = |
16 struct |
19 struct |