		Search-engine friendly clone of the ACL2 documentation.

Svexl

Svexl-p

Recognizer for svexl structures.

Signature
(svexl-p x) → *

Definitions and Theorems

Function: svexl-p

(defun svexl-p (x)
 (declare (xargs :guard t))
 (let ((acl2::__function__ 'svexl-p))
   (declare (ignorable acl2::__function__))
   (and (mbe :logic (and (alistp x)
                         (equal (strip-cars x)
                                '(top-node node-array)))
             :exec (fty::alist-with-carsp x '(top-node node-array)))
        (b* ((top-node (cdr (std::da-nth 0 x)))
             (node-array (cdr (std::da-nth 1 x))))
          (and (svexl-node-p top-node)
               (svexl-node-array-p node-array))))))

Theorem: consp-when-svexl-p

(defthm consp-when-svexl-p
  (implies (svexl-p x) (consp x))
  :rule-classes :compound-recognizer)