		Search-engine friendly clone of the ACL2 documentation.

Abstract-syntax-operations

Init-declor->ident

Identifier of an initializer declarator.

Signature
(init-declor->ident initdeclor) → ident
Arguments: initdeclor — Guard (init-declorp initdeclor).
Returns: ident — Type (identp ident).

Definitions and Theorems

Function: init-declor->ident

(defun init-declor->ident (initdeclor)
  (declare (xargs :guard (init-declorp initdeclor)))
  (b* (((init-declor initdeclor) initdeclor))
    (declor->ident initdeclor.declor)))

Theorem: identp-of-init-declor->ident

(defthm identp-of-init-declor->ident
  (b* ((ident (init-declor->ident initdeclor)))
    (identp ident))
  :rule-classes :rewrite)

Theorem: init-declor->ident-of-init-declor-fix-initdeclor

(defthm init-declor->ident-of-init-declor-fix-initdeclor
  (equal (init-declor->ident (init-declor-fix initdeclor))
         (init-declor->ident initdeclor)))

Theorem: init-declor->ident-init-declor-equiv-congruence-on-initdeclor

(defthm
      init-declor->ident-init-declor-equiv-congruence-on-initdeclor
  (implies (init-declor-equiv initdeclor initdeclor-equiv)
           (equal (init-declor->ident initdeclor)
                  (init-declor->ident initdeclor-equiv)))
  :rule-classes :congruence)