		Search-engine friendly clone of the ACL2 documentation.

Qualified-ident

Internal-ident

Signature
(internal-ident filepath ident) → qualified-ident
Arguments: filepath — Guard (filepathp filepath).; ident — Guard (identp ident).
Returns: qualified-ident — Type (qualified-identp qualified-ident).

Definitions and Theorems

Function: internal-ident

(defun internal-ident (filepath ident)
  (declare (xargs :guard (and (filepathp filepath)
                              (identp ident))))
  (let ((__function__ 'internal-ident))
    (declare (ignorable __function__))
    (make-qualified-ident :filepath? (c$::filepath-fix filepath)
                          :ident ident)))

Theorem: qualified-identp-of-internal-ident

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