Compose an identifier and an abstract function declarator into a function declarator.
(ident+adeclor-to-fun-declor id adeclor) → declor
This is the inverse of fun-declor-to-ident+adeclor.
Function:
(defun ident+adeclor-to-fun-declor (id adeclor) (declare (xargs :guard (and (identp id) (fun-adeclorp adeclor)))) (let ((__function__ 'ident+adeclor-to-fun-declor)) (declare (ignorable __function__)) (fun-adeclor-case adeclor :base (make-fun-declor-base :name id :params adeclor.params) :pointer (make-fun-declor-pointer :decl (ident+adeclor-to-fun-declor id adeclor.decl)))))
Theorem:
(defthm fun-declorp-of-ident+adeclor-to-fun-declor (b* ((declor (ident+adeclor-to-fun-declor id adeclor))) (fun-declorp declor)) :rule-classes :rewrite)
Theorem:
(defthm ident+adeclor-to-fun-declor-of-fun-declor-to-ident+adeclor (b* (((mv id adeclor) (fun-declor-to-ident+adeclor declor))) (equal (ident+adeclor-to-fun-declor id adeclor) (fun-declor-fix declor))))
Theorem:
(defthm fun-declor-to-ident+adeclor-of-ident+adeclor-to-fun-declor (equal (fun-declor-to-ident+adeclor (ident+adeclor-to-fun-declor id adeclor)) (mv (ident-fix id) (fun-adeclor-fix adeclor))))
Theorem:
(defthm ident+adeclor-to-fun-declor-of-ident-fix-id (equal (ident+adeclor-to-fun-declor (ident-fix id) adeclor) (ident+adeclor-to-fun-declor id adeclor)))
Theorem:
(defthm ident+adeclor-to-fun-declor-ident-equiv-congruence-on-id (implies (ident-equiv id id-equiv) (equal (ident+adeclor-to-fun-declor id adeclor) (ident+adeclor-to-fun-declor id-equiv adeclor))) :rule-classes :congruence)
Theorem:
(defthm ident+adeclor-to-fun-declor-of-fun-adeclor-fix-adeclor (equal (ident+adeclor-to-fun-declor id (fun-adeclor-fix adeclor)) (ident+adeclor-to-fun-declor id adeclor)))
Theorem:
(defthm ident+adeclor-to-fun-declor-fun-adeclor-equiv-congruence-on-adeclor (implies (fun-adeclor-equiv adeclor adeclor-equiv) (equal (ident+adeclor-to-fun-declor id adeclor) (ident+adeclor-to-fun-declor id adeclor-equiv))) :rule-classes :congruence)