		Search-engine friendly clone of the ACL2 documentation.

Specialize

Ident-from-paramdecl

Get the identifier from a parameter declaration.

Signature
(ident-from-paramdecl paramdecl) → ident
Arguments: paramdecl — Guard (paramdeclp paramdecl).
Returns: ident — Type (ident-optionp ident).

This may return nil when the parameter declaration is unnamed.

Definitions and Theorems

Function: ident-from-paramdecl

(defun ident-from-paramdecl (paramdecl)
  (declare (xargs :guard (paramdeclp paramdecl)))
  (let ((__function__ 'ident-from-paramdecl))
    (declare (ignorable __function__))
    (b* (((paramdecl paramdecl) paramdecl))
      (paramdeclor-case
           paramdecl.decl
           :declor (declor-get-ident paramdecl.decl.unwrap)
           :otherwise nil))))

Theorem: ident-optionp-of-ident-from-paramdecl

(defthm ident-optionp-of-ident-from-paramdecl
  (b* ((ident (ident-from-paramdecl paramdecl)))
    (ident-optionp ident))
  :rule-classes :rewrite)