		Search-engine friendly clone of the ACL2 documentation.

Symbolic-arithmetic

Aabf-first/rest/end

Signature
(aabf-first/rest/end x) → (mv first rest end)
Arguments: x — Guard (true-listp x).

Definitions and Theorems

Function: aabf-first/rest/end

(defun aabf-first/rest/end (x)
  (declare (xargs :guard (true-listp x)))
  (declare (xargs :guard (and)))
  (let ((__function__ 'aabf-first/rest/end))
    (declare (ignorable __function__))
    (mbe :logic (mv (aabf-car x) (scdr x) (s-endp x))
         :exec (cond ((atom x) (mv (aabf-false) x t))
                     ((atom (cdr x)) (mv (car x) x t))
                     (t (mv (car x) (cdr x) nil))))))

Theorem: trivial-theorem-about-aabf-first/rest/end

(defthm trivial-theorem-about-aabf-first/rest/end
  (b* nil
    (b* ((?ignore (aabf-first/rest/end x)))
      t))
  :rule-classes nil)