Recognizer for fgl-casesplit-config structures.
(fgl-casesplit-config-p x) → *
Function:
(defun fgl-casesplit-config-p (x) (declare (xargs :guard t)) (let ((__function__ 'fgl-casesplit-config-p)) (declare (ignorable __function__)) (and (mbe :logic (and (alistp x) (equal (strip-cars x) '(split-params solve-params split-concl repeat-concl allow-irrel-casesplit-vars cases fgl-config stop-on-ctrex stop-on-fail))) :exec (fty::alist-with-carsp x '(split-params solve-params split-concl repeat-concl allow-irrel-casesplit-vars cases fgl-config stop-on-ctrex stop-on-fail))) (b* ((?split-params (cdr (std::da-nth 0 x))) (?solve-params (cdr (std::da-nth 1 x))) (?split-concl (cdr (std::da-nth 2 x))) (?repeat-concl (cdr (std::da-nth 3 x))) (?allow-irrel-casesplit-vars (cdr (std::da-nth 4 x))) (cases (cdr (std::da-nth 5 x))) (fgl-config (cdr (std::da-nth 6 x))) (?stop-on-ctrex (cdr (std::da-nth 7 x))) (?stop-on-fail (cdr (std::da-nth 8 x)))) (and (casesplit-alist-p cases) (fgl-config-p fgl-config))))))
Theorem:
(defthm consp-when-fgl-casesplit-config-p (implies (fgl-casesplit-config-p x) (consp x)) :rule-classes :compound-recognizer)