		Search-engine friendly clone of the ACL2 documentation.

Qualified-ident

External-ident

Signature
(external-ident ident) → qualified-ident
Arguments: ident — Guard (identp ident).
Returns: qualified-ident — Type (qualified-identp qualified-ident).

Definitions and Theorems

Function: external-ident

(defun external-ident (ident)
  (declare (xargs :guard (identp ident)))
  (let ((__function__ 'external-ident))
    (declare (ignorable __function__))
    (make-qualified-ident :ident ident)))

Theorem: qualified-identp-of-external-ident

(defthm qualified-identp-of-external-ident
  (b* ((qualified-ident (external-ident ident)))
    (qualified-identp qualified-ident))
  :rule-classes :rewrite)