		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 (emptyp x)))))
  (mbe :logic (cdr (sfix x))
       :exec (cdr x)))

Theorem: tail-count

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

Theorem: tail-count-built-in

(defthm tail-count-built-in
  (implies (not (emptyp 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-emptyp

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

Theorem: tail-sfix-cancel

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