		Search-engine friendly clone of the ACL2 documentation.

Abstract-syntax-operations

Fundef->name

Name of a function in a definition.

Signature
(fundef->name fundef) → name
Arguments: fundef — Guard (fundefp fundef).
Returns: name — Type (identp name).

Definitions and Theorems

Function: fundef->name

(defun fundef->name (fundef)
  (declare (xargs :guard (fundefp fundef)))
  (let ((__function__ 'fundef->name))
    (declare (ignorable __function__))
    (b* (((mv name &)
          (fun-declor-to-ident+adeclor (fundef->declor fundef))))
      name)))

Theorem: identp-of-fundef->name

(defthm identp-of-fundef->name
  (b* ((name (fundef->name fundef)))
    (identp name))
  :rule-classes :rewrite)

Theorem: fundef->name-of-fundef-fix-fundef

(defthm fundef->name-of-fundef-fix-fundef
  (equal (fundef->name (fundef-fix fundef))
         (fundef->name fundef)))

Theorem: fundef->name-fundef-equiv-congruence-on-fundef

(defthm fundef->name-fundef-equiv-congruence-on-fundef
  (implies (fundef-equiv fundef fundef-equiv)
           (equal (fundef->name fundef)
                  (fundef->name fundef-equiv)))
  :rule-classes :congruence)