		Search-engine friendly clone of the ACL2 documentation.

Closure

Concatenation-called-rules

Rule names that occur in a concatenation.

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

Function: concatenation-called-rules

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