		Search-engine friendly clone of the ACL2 documentation.

Abstract-syntax-operations

Fun-declor-to-ident+adeclor

Decompose a function declarator into an identifier and an abstract function declarator.

Signature
(fun-declor-to-ident+adeclor declor) → (mv id adeclor)
Arguments: declor — Guard (fun-declorp declor).
Returns: id — Type (identp id).; adeclor — Type (fun-adeclorp adeclor).

This abstracts a function declarator to an abstract function declarator, by removing the identifier and also returning it. See fun-adeclor.

Definitions and Theorems

Function: fun-declor-to-ident+adeclor

(defun fun-declor-to-ident+adeclor (declor)
 (declare (xargs :guard (fun-declorp declor)))
 (let ((__function__ 'fun-declor-to-ident+adeclor))
  (declare (ignorable __function__))
  (fun-declor-case declor :base
                   (mv declor.name
                       (fun-adeclor-base declor.params))
                   :pointer
                   (b* (((mv id sub)
                         (fun-declor-to-ident+adeclor declor.decl)))
                     (mv id (fun-adeclor-pointer sub))))))

Theorem: identp-of-fun-declor-to-ident+adeclor.id

(defthm identp-of-fun-declor-to-ident+adeclor.id
  (b* (((mv acl2::?id ?adeclor)
        (fun-declor-to-ident+adeclor declor)))
    (identp id))
  :rule-classes :rewrite)

Theorem: fun-adeclorp-of-fun-declor-to-ident+adeclor.adeclor

(defthm fun-adeclorp-of-fun-declor-to-ident+adeclor.adeclor
  (b* (((mv acl2::?id ?adeclor)
        (fun-declor-to-ident+adeclor declor)))
    (fun-adeclorp adeclor))
  :rule-classes :rewrite)

Theorem: fun-declor-to-ident+adeclor-of-fun-declor-fix-declor

(defthm fun-declor-to-ident+adeclor-of-fun-declor-fix-declor
  (equal (fun-declor-to-ident+adeclor (fun-declor-fix declor))
         (fun-declor-to-ident+adeclor declor)))

Theorem: fun-declor-to-ident+adeclor-fun-declor-equiv-congruence-on-declor

(defthm
  fun-declor-to-ident+adeclor-fun-declor-equiv-congruence-on-declor
  (implies (fun-declor-equiv declor declor-equiv)
           (equal (fun-declor-to-ident+adeclor declor)
                  (fun-declor-to-ident+adeclor declor-equiv)))
  :rule-classes :congruence)