Major Section: ACL2-BUILT-INS
(String< str1 str2)
is non-nil
if and only if the string
str1
precedes the string str2
lexicographically, where
character inequalities are tested using char<
. When non-nil
,
(string< str1 str2)
is the first position (zero-based) at which
the strings differ. Here are some examples.
ACL2 !>(string< "abcd" "abu") 2 ACL2 !>(string< "abcd" "Abu") NIL ACL2 !>(string< "abc" "abcde") 3 ACL2 !>(string< "abcde" "abc") NIL
The guard for string<
specifies that its arguments are strings.
String<
is a Common Lisp function. See any Common Lisp
documentation for more information.
To see the ACL2 definition of this function, see pf.