		Search-engine friendly clone of the ACL2 documentation.

Bvec

First/rest/end

Deconstruct a signed bit vector.

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

Definitions and Theorems

Function: first/rest/end

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