		Search-engine friendly clone of the ACL2 documentation.

Abstract-syntax-aidentp

Ident-aidentp

Signature
(ident-aidentp ident gcc) → fty::result
Arguments: ident — Guard (identp ident).; gcc — Guard (booleanp gcc).
Returns: fty::result — Type (booleanp fty::result).

Definitions and Theorems

Function: ident-aidentp

(defun ident-aidentp (ident gcc)
  (declare (xargs :guard (and (identp ident) (booleanp gcc))))
  (declare (ignorable ident))
  (let ((__function__ 'ident-aidentp))
    (declare (ignorable __function__))
    (ascii-ident-stringp (ident->unwrap ident)
                         gcc)))

Theorem: booleanp-of-ident-aidentp

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

Theorem: ident-aidentp-of-ident-fix-ident

(defthm ident-aidentp-of-ident-fix-ident
  (equal (ident-aidentp (ident-fix ident) gcc)
         (ident-aidentp ident gcc)))

Theorem: ident-aidentp-ident-equiv-congruence-on-ident

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

Theorem: ident-aidentp-of-bool-fix-gcc

(defthm ident-aidentp-of-bool-fix-gcc
  (equal (ident-aidentp ident (bool-fix gcc))
         (ident-aidentp ident gcc)))

Theorem: ident-aidentp-iff-congruence-on-gcc

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