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.
