Recognizer for fty-type structures.
(fty-type-p x) → *
Function:
(defun fty-type-p (x) (declare (xargs :guard t)) (let ((acl2::__function__ 'fty-type-p)) (declare (ignorable acl2::__function__)) (and (consp x) (cond ((or (atom x) (eq (car x) :prod)) (and (true-listp (cdr x)) (eql (len (cdr x)) 1) (b* ((fields (std::da-nth 0 (cdr x)))) (fty-field-alist-p fields)))) ((eq (car x) :list) (and (true-listp (cdr x)) (eql (len (cdr x)) 1) (b* ((elt-type (std::da-nth 0 (cdr x)))) (symbolp elt-type)))) ((eq (car x) :alist) (and (true-listp (cdr x)) (eql (len (cdr x)) 2) (b* ((key-type (std::da-nth 0 (cdr x))) (val-type (std::da-nth 1 (cdr x)))) (and (symbolp key-type) (symbolp val-type))))) (t (and (eq (car x) :option) (and (true-listp (cdr x)) (eql (len (cdr x)) 1)) (b* ((some-type (std::da-nth 0 (cdr x)))) (symbolp some-type))))))))
Theorem:
(defthm consp-when-fty-type-p (implies (fty-type-p x) (consp x)) :rule-classes :compound-recognizer)