		Search-engine friendly clone of the ACL2 documentation.

Well-formedness

Rule-list-wfp

Check if all the rules in a list of rules are well-formed.

Signature
(rule-list-wfp x) → std::bool

This is an ordinary std::deflist. It is "loose" in that it does not care whether x is nil-terminated.

Definitions and Theorems

Function: rule-list-wfp

(defun rule-list-wfp (x)
  (declare (xargs :guard (rulelistp x)))
  (let ((__function__ 'rule-list-wfp))
    (declare (ignorable __function__))
    (if (consp x)
        (and (rule-wfp (car x))
             (rule-list-wfp (cdr x)))
      t)))

Subtopics

Rule-list-wfp-basics: Basic theorems about rule-list-wfp, generated by std::deflist.