		Search-engine friendly clone of the ACL2 documentation.

Rule-utilities

Rulenames-from-singular-conc-and-rep

Signature
(rulenames-from-singular-conc-and-rep concs) → rulenames
Arguments: concs — Guard (alternationp concs).
Returns: rulenames — Type (acl2::string-list-resultp rulenames).

Definitions and Theorems

Function: rulenames-from-singular-conc-and-rep

(defun rulenames-from-singular-conc-and-rep (concs)
 (declare (xargs :guard (alternationp concs)))
 (let ((__function__ 'rulenames-from-singular-conc-and-rep))
  (declare (ignorable __function__))
  (b*
   (((when (endp concs)) nil)
    (first-conc (first concs))
    ((unless (equal (len first-conc) 1))
     (reserrf (cons :concatenation-is-not-singular first-conc)))
    (the-rep (car first-conc))
    ((unless
      (and
       (repetitionp the-rep)
       (numrep-match-repeat-range-p 1 (repetition->range the-rep))))
     (reserrf (cons :not-singular-repetition the-rep)))
    (the-el (repetition->element the-rep))
    ((unless (and (elementp the-el)
                  (element-case the-el :rulename)))
     (reserrf (cons :not-rulename-element the-el)))
    (rest-rulenames
         (rulenames-from-singular-conc-and-rep (rest concs)))
    ((when (reserrp rest-rulenames))
     rest-rulenames)
    ((unless (string-listp rest-rulenames))
     (reserrf (cons :impossible rest-rulenames))))
   (cons (str-fix (rulename->get (element-rulename->get the-el)))
         rest-rulenames))))

Theorem: string-list-resultp-of-rulenames-from-singular-conc-and-rep

(defthm string-list-resultp-of-rulenames-from-singular-conc-and-rep
  (b* ((rulenames (rulenames-from-singular-conc-and-rep concs)))
    (acl2::string-list-resultp rulenames))
  :rule-classes :rewrite)