		Search-engine friendly clone of the ACL2 documentation.

Primitives

Tail

(tail x) returns the remainder of a set after removing its head.

This is like cdr, but respects the non-set convention and always returns nil for ill-formed sets.

Definitions and Theorems

Function: tail

(defun tail (x)
       (declare (xargs :guard (and (setp x) (not (empty x)))))
       (mbe :logic (cdr (sfix x))
            :exec (cdr x)))

Theorem: tail-count

(defthm tail-count
        (implies (not (empty x))
                 (< (acl2-count (tail x))
                    (acl2-count x)))
        :rule-classes ((:rewrite) (:linear)))

Theorem: tail-count-built-in

(defthm tail-count-built-in
        (implies (not (empty x))
                 (o< (acl2-count (tail x))
                     (acl2-count x)))
        :rule-classes :built-in-clause)

Theorem: tail-produces-set

(defthm tail-produces-set (setp (tail x)))

Theorem: tail-when-empty

(defthm tail-when-empty
        (implies (empty x)
                 (equal (tail x) nil)))

Theorem: tail-sfix-cancel

(defthm tail-sfix-cancel
        (equal (tail (sfix x)) (tail x)))