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