		Search-engine friendly clone of the ACL2 documentation.

Abstract-syntax-operations

Obj-declor-to-ident+adeclor

Decompose an object declarator into an identifier and an abstract object declarator.

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

This abstracts an object declarator to an abstract object declarator, by removing the identifier and also returning it. See obj-adeclor.

Definitions and Theorems

Function: obj-declor-to-ident+adeclor

(defun obj-declor-to-ident+adeclor (declor)
  (declare (xargs :guard (obj-declorp declor)))
  (let ((__function__ 'obj-declor-to-ident+adeclor))
    (declare (ignorable __function__))
    (obj-declor-case
         declor :ident
         (mv declor.get (obj-adeclor-none))
         :pointer
         (b* (((mv id sub)
               (obj-declor-to-ident+adeclor declor.decl)))
           (mv id
               (make-obj-adeclor-pointer :decl sub)))
         :array
         (b* (((mv id sub)
               (obj-declor-to-ident+adeclor declor.decl)))
           (mv id
               (make-obj-adeclor-array :decl sub
                                       :size declor.size))))))

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

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

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

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

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

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

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

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