		Search-engine friendly clone of the ACL2 documentation.

Mapping-to-language-definition

Ldm-tyname

Map a type name to a type name in the language definition.

Signature
(ldm-tyname tyname) → (mv erp tyname1)
Arguments: tyname — Guard (tynamep tyname).
Returns: tyname1 — Type (c::tynamep tyname1).

The specifiers and qualifiers must be all type specifiers, and must form a supported sequence.

Definitions and Theorems

Function: ldm-tyname

(defun ldm-tyname (tyname)
 (declare (xargs :guard (tynamep tyname)))
 (declare (xargs :guard (tyname-unambp tyname)))
 (let ((__function__ 'ldm-tyname))
  (declare (ignorable __function__))
  (b*
   (((reterr)
     (c::tyname (c::tyspecseq-void)
                (c::obj-adeclor-none)))
    ((tyname tyname) tyname)
    ((mv okp tyspecs)
     (check-spec/qual-list-all-typespec tyname.specqual))
    ((when (not okp))
     (reterr
      (msg
       "Unsupported specifiers and qualifiers ~
                      in type name ~x0."
       (tyname-fix tyname))))
    ((erp tyspecseq)
     (ldm-type-spec-list tyspecs))
    ((when (not tyname.decl?))
     (retok (c::make-tyname :tyspec tyspecseq
                            :declor (c::obj-adeclor-none))))
    ((erp adeclor1)
     (ldm-absdeclor-obj tyname.decl?)))
   (retok (c::make-tyname :tyspec tyspecseq
                          :declor adeclor1)))))

Theorem: tynamep-of-ldm-tyname.tyname1

(defthm tynamep-of-ldm-tyname.tyname1
  (b* (((mv acl2::?erp ?tyname1)
        (ldm-tyname tyname)))
    (c::tynamep tyname1))
  :rule-classes :rewrite)

Theorem: ldm-tyname-of-tyname-fix-tyname

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

Theorem: ldm-tyname-tyname-equiv-congruence-on-tyname

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