Recognizer for svexllist structures.
(svexllist-p x) → *
Function:
(defun svexllist-p (x) (declare (xargs :guard t)) (let ((acl2::__function__ 'svexllist-p)) (declare (ignorable acl2::__function__)) (and (mbe :logic (and (alistp x) (equal (strip-cars x) '(top-nodelist node-array))) :exec (fty::alist-with-carsp x '(top-nodelist node-array))) (b* ((top-nodelist (cdr (std::da-nth 0 x))) (node-array (cdr (std::da-nth 1 x)))) (and (svexl-nodelist-p top-nodelist) (svexl-node-array-p node-array))))))
Theorem:
(defthm consp-when-svexllist-p (implies (svexllist-p x) (consp x)) :rule-classes :compound-recognizer)