		Search-engine friendly clone of the ACL2 documentation.

Convenience-constructors

/_-fn

Signature
(/_-fn xs) → concatenation
Arguments: xs — Guard (repetition/element/rulename/charstring-listp xs).
Returns: concatenation — Type (concatenationp concatenation).

Definitions and Theorems

Function: /_-fn

(defun /_-fn (xs)
 (declare
   (xargs :guard (repetition/element/rulename/charstring-listp xs)))
 (cond
  ((endp xs) nil)
  (t
   (b*
    ((x (car xs))
     (range1 (make-repeat-range :min 1
                                :max (nati-finite 1)))
     (repetition
      (cond
       ((elementp x)
        (make-repetition :range range1
                         :element x))
       ((rulenamep x)
        (make-repetition :range range1
                         :element (element-rulename x)))
       ((common-lisp::stringp x)
        (make-repetition
          :range range1
          :element (element-char-val (char-val-insensitive nil x))))
       (t (repetition-fix x)))))
    (cons repetition (/_-fn (cdr xs)))))))

Theorem: concatenationp-of-/_-fn

(defthm concatenationp-of-/_-fn
  (b* ((concatenation (/_-fn xs)))
    (concatenationp concatenation))
  :rule-classes :rewrite)