SUBSEQ

subsequence of a string or list
Major Section:  ACL2-BUILT-INS

For any natural numbers start and end, where start <= end <= (length seq), (subseq seq start end) is the subsequence of seq from index start up to, but not including, index end. End may be nil, which which case it is treated as though it is (length seq), i.e., we obtain the subsequence of seq from index start all the way to the end.

The guard for (subseq seq start end) is that seq is a true list or a string, start and end are integers (except, end may be nil, in which case it is treated as (length seq) for the rest of this discussion), and 0 <= start <= end <= (length seq).

Subseq is a Common Lisp function. See any Common Lisp documentation for more information. Note: In Common Lisp the third argument of subseq is optional, but in ACL2 it is required, though it may be nil as explained above.

To see the ACL2 definition of this function, see pf.