STRING<

less-than test for strings
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.