		Search-engine friendly clone of the ACL2 documentation.

Well-formedness

Concatenation-list-wfp

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

Signature
(concatenation-list-wfp concatenations) → yes/no
Arguments: concatenations — Guard (alternationp concatenations).
Returns: yes/no — Type (booleanp yes/no).

Function: concatenation-list-wfp

(defun concatenation-list-wfp (concatenations)
  (declare (xargs :guard (alternationp concatenations)))
  (or (endp concatenations)
      (and (concatenation-wfp (car concatenations))
           (concatenation-list-wfp (cdr concatenations)))))

Subtopics

Concatenation-list-wfp-basics: Basic theorems about concatenation-list-wfp, generated by std::deflist.