		Search-engine friendly clone of the ACL2 documentation.

Primitives

Head

(head x) returns the smallest element in a set.

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

Definitions and Theorems

Function: head

(defun head (x)
  (declare (xargs :guard (and (setp x) (not (emptyp x)))))
  (mbe :logic (car (sfix x))
       :exec (car x)))

Theorem: head-count

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

Theorem: head-count-built-in

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

Theorem: head-when-emptyp

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

Theorem: head-sfix-cancel

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

Theorem: head-minimal

(defthm head-minimal
  (implies (<< a (head x))
           (not (in a x))))

Theorem: head-minimal-2

(defthm head-minimal-2
  (implies (in a x)
           (not (<< a (head x)))))

Theorem: head-unique

(defthm head-unique
  (not (in (head x) (tail x))))