		Search-engine friendly clone of the ACL2 documentation.

Split

Vl-nosplit-p

Recognize an expression that is may as well be atomic for the purposes of split.

Signature
(vl-nosplit-p x) → *
Arguments: x — Guard (vl-expr-p x).

This is almost just vl-expr-sliceable-p, except that there are some atomic expressions (e.g., real numbers, strings, etc.) that aren't sliceable, but that we still don't want to split up.

Definitions and Theorems

Function: vl-nosplit-p$inline

(defun vl-nosplit-p$inline (x)
  (declare (xargs :guard (vl-expr-p x)))
  (let ((__function__ 'vl-nosplit-p))
    (declare (ignorable __function__))
    (if (vl-fast-atom-p x)
        t
      (vl-expr-sliceable-p x))))