Subseq
Subsequence of a string or list
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, in 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.
Function: subseq
(defun subseq (seq start end)
(declare (xargs :guard (and (or (true-listp seq) (stringp seq))
(integerp start)
(<= 0 start)
(or (null end)
(and (integerp end)
(<= end (length seq))))
(<= start (or end (length seq))))))
(if (stringp seq)
(coerce (subseq-list (coerce seq 'list)
start (or end (length seq)))
'string)
(subseq-list seq start (or end (length seq)))))Subtopics
- Subseq-list
- Lemmas about subseq-list available in the std/lists
library.
