		Search-engine friendly clone of the ACL2 documentation.

Mapping-to-language-definition

Ldm-paramdeclor

Map a parameter declarator to an object declarator in the language definition.

Signature
(ldm-paramdeclor paramdeclor) → (mv erp objdeclor)
Arguments: paramdeclor — Guard (paramdeclorp paramdeclor).
Returns: objdeclor — Type (c::obj-declorp objdeclor).

The parameter declarator must be present and not abstract. The declarator must be for an object, which we map to an object declarator.

Definitions and Theorems

Function: ldm-paramdeclor

(defun ldm-paramdeclor (paramdeclor)
 (declare (xargs :guard (paramdeclorp paramdeclor)))
 (declare (xargs :guard (paramdeclor-unambp paramdeclor)))
 (let ((__function__ 'ldm-paramdeclor))
  (declare (ignorable __function__))
  (b*
   (((reterr)
     (c::obj-declor-ident (c::ident "irrelevant")))
    ((when (paramdeclor-case paramdeclor :absdeclor))
     (reterr
      (msg
       "Unsupported parameter declarator ~x0 ~
                      with abstract declarator."
       (paramdeclor-fix paramdeclor))))
    ((when (paramdeclor-case paramdeclor :none))
     (reterr (msg "Unsupported absent parameter declarator ~x0.")))
    ((when (paramdeclor-case paramdeclor :ambig))
     (prog2$ (impossible) (reterr t)))
    (declor (paramdeclor-declor->unwrap paramdeclor)))
   (ldm-declor-obj declor))))

Theorem: obj-declorp-of-ldm-paramdeclor.objdeclor

(defthm obj-declorp-of-ldm-paramdeclor.objdeclor
  (b* (((mv acl2::?erp ?objdeclor)
        (ldm-paramdeclor paramdeclor)))
    (c::obj-declorp objdeclor))
  :rule-classes :rewrite)

Theorem: ldm-paramdeclor-of-paramdeclor-fix-paramdeclor

(defthm ldm-paramdeclor-of-paramdeclor-fix-paramdeclor
  (equal (ldm-paramdeclor (paramdeclor-fix paramdeclor))
         (ldm-paramdeclor paramdeclor)))

Theorem: ldm-paramdeclor-paramdeclor-equiv-congruence-on-paramdeclor

(defthm ldm-paramdeclor-paramdeclor-equiv-congruence-on-paramdeclor
  (implies (paramdeclor-equiv paramdeclor paramdeclor-equiv)
           (equal (ldm-paramdeclor paramdeclor)
                  (ldm-paramdeclor paramdeclor-equiv)))
  :rule-classes :congruence)