Recognizer for vl-bindelim-institem structures.
(vl-bindelim-institem-p x) → *
Function:
(defun vl-bindelim-institem-p (x) (declare (xargs :guard t)) (let ((__function__ 'vl-bindelim-institem-p)) (declare (ignorable __function__)) (and (std::prod-consp x) (std::prod-consp (std::prod-car x)) (std::prod-consp (std::prod-cdr x)) (b* ((inst (std::prod-car (std::prod-car x))) (genp (std::prod-cdr (std::prod-car x))) (bindp (std::prod-car (std::prod-cdr x))) (ctx (std::prod-cdr (std::prod-cdr x)))) (and (vl-modinst-p inst) (booleanp genp) (booleanp bindp) (vl-bindcontext-p ctx))))))