		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)))
  (b* ((idents (ident-set-fix idents))
       ((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)

Theorem: map-ident->unwrap-of-ident-set-fix-idents

(defthm map-ident->unwrap-of-ident-set-fix-idents
  (equal (map-ident->unwrap (ident-set-fix idents))
         (map-ident->unwrap idents)))

Theorem: map-ident->unwrap-ident-set-equiv-congruence-on-idents

(defthm map-ident->unwrap-ident-set-equiv-congruence-on-idents
  (implies (c$::ident-set-equiv idents idents-equiv)
           (equal (map-ident->unwrap idents)
                  (map-ident->unwrap idents-equiv)))
  :rule-classes :congruence)