		Search-engine friendly clone of the ACL2 documentation.

Call-graphs

Direct-fun-refp

Signature
(direct-fun-refp ident valid-table) → *
Arguments: ident — Guard (identp ident).; valid-table — Guard (c$::valid-tablep valid-table).

Definitions and Theorems

Function: direct-fun-refp

(defun direct-fun-refp (ident valid-table)
 (declare (xargs :guard (and (identp ident)
                             (c$::valid-tablep valid-table))))
 (declare (xargs :type-prescription
                 (booleanp (direct-fun-refp ident valid-table))))
 (let ((__function__ 'direct-fun-refp))
   (declare (ignorable __function__))
   (b* ((info? (c$::valid-lookup-ord-file-scope ident valid-table)))
     (and info?
          (c$::valid-ord-info-case info?
                                   :objfun t
                                   :otherwise nil)))))