less-than-or-equal 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 or the strings are equal. When non-nil, (string<= str1 str2) is the first position (zero-based) at which the strings differ, if they differ, and otherwise is their common length. See string<.

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.