		Search-engine friendly clone of the ACL2 documentation.

Fresh-ident-utility

Map-ident->unwrap

Signature
(map-ident->unwrap idents) → strings
Arguments: idents — Guard (ident-setp idents).
Returns: strings — Type (acl2::string-setp strings).

Definitions and Theorems

Function: map-ident->unwrap

(defun map-ident->unwrap (idents)
  (declare (xargs :guard (ident-setp idents)))
  (let ((__function__ 'map-ident->unwrap))
    (declare (ignorable __function__))
    (b* (((when (emptyp idents)) nil)
         (unwrapped-head (ident->unwrap (head idents))))
      (if (stringp unwrapped-head)
          (insert unwrapped-head
                  (map-ident->unwrap (tail idents)))
        (map-ident->unwrap (tail idents))))))

Theorem: string-setp-of-map-ident->unwrap

(defthm string-setp-of-map-ident->unwrap
  (b* ((strings (map-ident->unwrap idents)))
    (acl2::string-setp strings))
  :rule-classes :rewrite)