		Search-engine friendly clone of the ACL2 documentation.

Specialize-implementation

Ident-from-param-declon

Get the identifier from a parameter declaration.

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

This may return nil when the parameter declaration is unnamed.

Definitions and Theorems

Function: ident-from-param-declon

(defun ident-from-param-declon (paramdecl)
  (declare (xargs :guard (param-declonp paramdecl)))
  (b* (((param-declon paramdecl) paramdecl))
    (param-declor-case
         paramdecl.declor
         :nonabstract (declor->ident paramdecl.declor.declor)
         :otherwise nil)))

Theorem: ident-optionp-of-ident-from-param-declon

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