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