		Search-engine friendly clone of the ACL2 documentation.

Well-formedness

Alternation-wfp

An alternation is well-formed iff it is not empty and all its concatenations are well-formed.

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

This non-emptiness condition is required by the rule alternation in [RFC:4]. The well-formedness condition on the concatenations is structural.

Function: alternation-wfp

(defun alternation-wfp (alternation)
  (declare (xargs :guard (alternationp alternation)))
  (and (consp alternation)
       (concatenation-list-wfp alternation)))