FTY version of check-list-call.
(fty-check-list-call term) → (mv yes/no elements)
Function:
(defun fty-check-list-call (term) (declare (xargs :guard (pseudo-termp term))) (let ((__function__ 'fty-check-list-call)) (declare (ignorable __function__)) (check-list-call (pseudo-term-fix term))))
Theorem:
(defthm booleanp-of-fty-check-list-call.yes/no (b* (((mv ?yes/no ?elements) (fty-check-list-call term))) (booleanp yes/no)) :rule-classes :rewrite)
Theorem:
(defthm pseudo-term-listp-of-fty-check-list-call.elements (b* (((mv ?yes/no ?elements) (fty-check-list-call term))) (pseudo-term-listp elements)) :rule-classes :rewrite)
Theorem:
(defthm true-listp-of-fty-check-list-call.elements (b* (((mv ?yes/no ?elements) (fty-check-list-call term))) (true-listp elements)) :rule-classes :type-prescription)