		Search-engine friendly clone of the ACL2 documentation.

Abstract-syntax-operations

Param-declon-to-ident+tyname

Decompose a parameter declaration into an identifier and a type name.

Signature
(param-declon-to-ident+tyname declon) → (mv id tyname)
Arguments: declon — Guard (param-declonp declon).
Returns: id — Type (identp id).; tyname — Type (tynamep tyname).

Definitions and Theorems

Function: param-declon-to-ident+tyname

(defun param-declon-to-ident+tyname (declon)
  (declare (xargs :guard (param-declonp declon)))
  (let ((__function__ 'param-declon-to-ident+tyname))
    (declare (ignorable __function__))
    (b* (((param-declon declon) declon))
      (tyspec+declor-to-ident+tyname declon.tyspec declon.declor))))

Theorem: identp-of-param-declon-to-ident+tyname.id

(defthm identp-of-param-declon-to-ident+tyname.id
  (b* (((mv acl2::?id ?tyname)
        (param-declon-to-ident+tyname declon)))
    (identp id))
  :rule-classes :rewrite)

Theorem: tynamep-of-param-declon-to-ident+tyname.tyname

(defthm tynamep-of-param-declon-to-ident+tyname.tyname
  (b* (((mv acl2::?id ?tyname)
        (param-declon-to-ident+tyname declon)))
    (tynamep tyname))
  :rule-classes :rewrite)

Theorem: param-declon-to-ident+tyname-of-param-declon-fix-declon

(defthm param-declon-to-ident+tyname-of-param-declon-fix-declon
  (equal (param-declon-to-ident+tyname (param-declon-fix declon))
         (param-declon-to-ident+tyname declon)))

Theorem: param-declon-to-ident+tyname-param-declon-equiv-congruence-on-declon

(defthm
 param-declon-to-ident+tyname-param-declon-equiv-congruence-on-declon
 (implies (param-declon-equiv declon declon-equiv)
          (equal (param-declon-to-ident+tyname declon)
                 (param-declon-to-ident+tyname declon-equiv)))
 :rule-classes :congruence)