Major Section: ACL2-BUILT-INS
Example Forms: (search "cd" "Cdabcdefcde") ; = 4, index of first match (search "cd" "Cdabcdefcde" :test 'equal) ; same as above (search "cd" "Cdabcdefcde" :from-end t) ; = 8, index of last match (search "cd" "Cdabcdefcde" :start1 1) ; = 1 (search "cd" "Cdabcdefcde" :start2 5) ; = 8 (search "cd" "Cdabcdefcde" :test 'char-equal) ; = 0 (case-insensitive) (search "ac" "Cdabcdefcde") ; = nil (search '(a b) '(9 8 a b 7 6)) ; = 2 General Form: (search seq1 seq2 &key from-end test start1 start2 end1 end2)
Search indicates whether one string or list occurs as a (contiguous)
subsequence of another string or list, respectively. It returns
no such match is found; otherwise it returns the (zero-based) index of the
first match by default, but a non-
nil value of keyword argument
:from-end causes it to return the last match. The
by default. The other legal value for
char-equal, which can
be given only for two strings, in which case the match is case-insensitive.
Finally, values of
:end1 for the first sequence, and of
:end2 for the second sequence, bound the portion of the
respective sequence used for deciding on a match, though the index returned
is always an index into the second sequence as a whole.
The guard for calls of
search is given by a function,
search-fn-guard, which has the following requirements.
o The two arguments much both satisfy
true-listpor else must both be strings, which must consist of standard characters (see standard-char-p) if the
:testmust evaluate to one of the symbols
char-equal, where the latter is only allowed if the (first) two arguments are strings.
o The values of
:end2must all be natural numbers, where if omitted they default to 0, 0, the length
len1of the first argument, and the length
len2of the second argument, respectively.
start1is the value of
:start1, defaulting as described just above, and similarly for the other start and end keywords and for lengths
len2as described just above, then:
start1 <= end1 <= len1and
start2 <= end2 <= len2.
Search is a Common Lisp function (actually, a macro in ACL2). See
any Common Lisp documentation for more information.