		Search-engine friendly clone of the ACL2 documentation.

Atc-function-and-loop-generation

Atc-formal-affectable-listp

Lift atc-formal-affectablep to lists.

Signature
(atc-formal-affectable-listp x typed-formals) → std::bool

This is an ordinary std::deflist. It is "strict" in that it requires x to be a "properly" nil-terminated list.

Definitions and Theorems

Function: atc-formal-affectable-listp

(defun atc-formal-affectable-listp (x typed-formals)
 (declare
     (xargs :guard (and (symbol-listp x)
                        (atc-symbol-varinfo-alistp typed-formals))))
 (let ((__function__ 'atc-formal-affectable-listp))
   (declare (ignorable __function__))
   (if (consp x)
       (and (atc-formal-affectablep (car x)
                                    typed-formals)
            (atc-formal-affectable-listp (cdr x)
                                         typed-formals))
     (null x))))

Subtopics

Atc-formal-affectable-listp-basics: Basic theorems about atc-formal-affectable-listp, generated by std::deflist.