		Search-engine friendly clone of the ACL2 documentation.

Splitgso-input-processing

Ident-map

Signature
(ident-map strings) → idents
Arguments: strings — Guard (string-listp strings).
Returns: idents — Type (ident-listp idents).

Definitions and Theorems

Function: ident-map

(defun ident-map (strings)
  (declare (xargs :guard (string-listp strings)))
  (let ((__function__ 'ident-map))
    (declare (ignorable __function__))
    (if (endp strings)
        nil
      (cons (ident (first strings))
            (ident-map (rest strings))))))

Theorem: ident-listp-of-ident-map

(defthm ident-listp-of-ident-map
  (b* ((idents (ident-map strings)))
    (ident-listp idents))
  :rule-classes :rewrite)