Recognizer for atj-function-type-info structures.
(atj-function-type-info-p x) → *
Function:
(defun atj-function-type-info-p (x) (declare (xargs :guard t)) (let ((__function__ 'atj-function-type-info-p)) (declare (ignorable __function__)) (and (true-listp x) (eql (len x) 2) (b* ((main (std::da-nth 0 x)) (others (std::da-nth 1 x))) (and (atj-function-type-p main) (atj-function-type-listp others))))))
Theorem:
(defthm consp-when-atj-function-type-info-p (implies (atj-function-type-info-p x) (consp x)) :rule-classes :compound-recognizer)