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