		Search-engine friendly clone of the ACL2 documentation.

Call-graphs

Qualify-ident

Signature
(qualify-ident filepath valid-table ident) → qualified-ident
Arguments: filepath — Guard (filepathp filepath).; valid-table — Guard (c$::valid-tablep valid-table).; ident — Guard (identp ident).
Returns: qualified-ident — Type (qualified-identp qualified-ident).

Definitions and Theorems

Function: qualify-ident

(defun qualify-ident (filepath valid-table ident)
 (declare (xargs :guard (and (filepathp filepath)
                             (c$::valid-tablep valid-table)
                             (identp ident))))
 (let ((__function__ 'qualify-ident))
  (declare (ignorable __function__))
  (b*
   ((info? (valid-table-global-lookup ident valid-table))
    (is-internal
     (and
      info?
      (c$::valid-ord-info-case
           info?
           :objfun (equal (c$::valid-ord-info-objfun->linkage info?)
                          (c$::linkage-internal))
           :otherwise nil))))
   (if is-internal (internal-ident filepath ident)
     (external-ident ident)))))

Theorem: qualified-identp-of-qualify-ident

(defthm qualified-identp-of-qualify-ident
  (b* ((qualified-ident (qualify-ident filepath valid-table ident)))
    (qualified-identp qualified-ident))
  :rule-classes :rewrite)