Deconstruct a signed bit vector.
(first/rest/end x) → (mv * * *)
Function:
(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))))))