		Search-engine friendly clone of the ACL2 documentation.

Abstract-syntax-collect-idents

Ext-declon-list-collect-idents

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

Definitions and Theorems

Function: ext-declon-list-collect-idents

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

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

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

Theorem: ext-declon-list-collect-idents-of-ext-declon-list-fix-ext-declon-list

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

Theorem: ext-declon-list-collect-idents-ext-declon-list-equiv-congruence-on-ext-declon-list

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