		Search-engine friendly clone of the ACL2 documentation.

Well-formedness

Repetition-wfp

A repetition is well-formed iff its repetition range and its element are well-formed.

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

This condition is structural.

Function: repetition-wfp

(defun repetition-wfp (repetition)
  (declare (xargs :guard (repetitionp repetition)))
  (and (repeat-range-wfp (repetition->range repetition))
       (element-wfp (repetition->element repetition))))