		Search-engine friendly clone of the ACL2 documentation.

Abstract-syntax-collect-idents

Ident-list-collect-idents

Signature
(ident-list-collect-idents c$::ident-list) → fty::result
Arguments: c$::ident-list — Guard (ident-listp c$::ident-list).
Returns: fty::result — Type (ident-setp fty::result).

Definitions and Theorems

Function: ident-list-collect-idents

(defun ident-list-collect-idents (c$::ident-list)
 (declare (xargs :guard (ident-listp c$::ident-list)))
 (let ((__function__ 'ident-list-collect-idents))
  (declare (ignorable __function__))
  (cond
     ((endp c$::ident-list) nil)
     (t (union (ident-collect-idents (car c$::ident-list))
               (ident-list-collect-idents (cdr c$::ident-list)))))))

Theorem: ident-setp-of-ident-list-collect-idents

(defthm ident-setp-of-ident-list-collect-idents
  (b* ((fty::result (ident-list-collect-idents c$::ident-list)))
    (ident-setp fty::result))
  :rule-classes :rewrite)

Theorem: ident-list-collect-idents-of-ident-list-fix-ident-list

(defthm ident-list-collect-idents-of-ident-list-fix-ident-list
 (equal
     (ident-list-collect-idents (c$::ident-list-fix c$::ident-list))
     (ident-list-collect-idents c$::ident-list)))

Theorem: ident-list-collect-idents-ident-list-equiv-congruence-on-ident-list

(defthm
 ident-list-collect-idents-ident-list-equiv-congruence-on-ident-list
 (implies (c$::ident-list-equiv c$::ident-list ident-list-equiv)
          (equal (ident-list-collect-idents c$::ident-list)
                 (ident-list-collect-idents ident-list-equiv)))
 :rule-classes :congruence)