		Search-engine friendly clone of the ACL2 documentation.

Abstract-syntax-aidentp

Extdecl-list-aidentp

Signature
(extdecl-list-aidentp extdecl-list gcc) → fty::result
Arguments: extdecl-list — Guard (extdecl-listp extdecl-list).; gcc — Guard (booleanp gcc).
Returns: fty::result — Type (booleanp fty::result).

Definitions and Theorems

Function: extdecl-list-aidentp

(defun extdecl-list-aidentp (extdecl-list gcc)
  (declare (xargs :guard (and (extdecl-listp extdecl-list)
                              (booleanp gcc))))
  (let ((__function__ 'extdecl-list-aidentp))
    (declare (ignorable __function__))
    (cond ((endp extdecl-list) t)
          (t (and (extdecl-aidentp (car extdecl-list) gcc)
                  (extdecl-list-aidentp (cdr extdecl-list)
                                        gcc))))))

Theorem: booleanp-of-extdecl-list-aidentp

(defthm booleanp-of-extdecl-list-aidentp
  (b* ((fty::result (extdecl-list-aidentp extdecl-list gcc)))
    (booleanp fty::result))
  :rule-classes :rewrite)

Theorem: extdecl-list-aidentp-of-extdecl-list-fix-extdecl-list

(defthm extdecl-list-aidentp-of-extdecl-list-fix-extdecl-list
  (equal (extdecl-list-aidentp (extdecl-list-fix extdecl-list)
                               gcc)
         (extdecl-list-aidentp extdecl-list gcc)))

Theorem: extdecl-list-aidentp-extdecl-list-equiv-congruence-on-extdecl-list

(defthm
 extdecl-list-aidentp-extdecl-list-equiv-congruence-on-extdecl-list
 (implies (extdecl-list-equiv extdecl-list extdecl-list-equiv)
          (equal (extdecl-list-aidentp extdecl-list gcc)
                 (extdecl-list-aidentp extdecl-list-equiv gcc)))
 :rule-classes :congruence)

Theorem: extdecl-list-aidentp-of-bool-fix-gcc

(defthm extdecl-list-aidentp-of-bool-fix-gcc
  (equal (extdecl-list-aidentp extdecl-list (bool-fix gcc))
         (extdecl-list-aidentp extdecl-list gcc)))

Theorem: extdecl-list-aidentp-iff-congruence-on-gcc

(defthm extdecl-list-aidentp-iff-congruence-on-gcc
  (implies (iff gcc gcc-equiv)
           (equal (extdecl-list-aidentp extdecl-list gcc)
                  (extdecl-list-aidentp extdecl-list gcc-equiv)))
  :rule-classes :congruence)