		Search-engine friendly clone of the ACL2 documentation.

Closure

Alternation-called-rules

Rule names that occur in an alternation.

Signature
(alternation-called-rules alternation) → rulenames
Arguments: alternation — Guard (alternationp alternation).
Returns: rulenames — Type (rulename-setp rulenames).

Function: alternation-called-rules

(defun alternation-called-rules (alternation)
  (declare (xargs :guard (alternationp alternation)))
  (cond ((endp alternation) nil)
        (t (union (concatenation-called-rules (car alternation))
                  (alternation-called-rules (cdr alternation))))))