		Search-engine friendly clone of the ACL2 documentation.

Static-semantics

Fun-table-lookup

Look up a function in a function table.

Signature
(fun-table-lookup fun funtab) → info
Arguments: fun — Guard (identp fun).; funtab — Guard (fun-tablep funtab).
Returns: info — Type (fun-sinfo-optionp info).

We return the type of the function, if the function is present. Otherwise, we return nil.

Definitions and Theorems

Function: fun-table-lookup

(defun fun-table-lookup (fun funtab)
  (declare (xargs :guard (and (identp fun) (fun-tablep funtab))))
  (let ((__function__ 'fun-table-lookup))
    (declare (ignorable __function__))
    (cdr (omap::assoc (ident-fix fun)
                      (fun-table-fix funtab)))))

Theorem: fun-sinfo-optionp-of-fun-table-lookup

(defthm fun-sinfo-optionp-of-fun-table-lookup
  (b* ((info (fun-table-lookup fun funtab)))
    (fun-sinfo-optionp info))
  :rule-classes :rewrite)

Theorem: fun-table-lookup-of-ident-fix-fun

(defthm fun-table-lookup-of-ident-fix-fun
  (equal (fun-table-lookup (ident-fix fun)
                           funtab)
         (fun-table-lookup fun funtab)))

Theorem: fun-table-lookup-ident-equiv-congruence-on-fun

(defthm fun-table-lookup-ident-equiv-congruence-on-fun
  (implies (ident-equiv fun fun-equiv)
           (equal (fun-table-lookup fun funtab)
                  (fun-table-lookup fun-equiv funtab)))
  :rule-classes :congruence)

Theorem: fun-table-lookup-of-fun-table-fix-funtab

(defthm fun-table-lookup-of-fun-table-fix-funtab
  (equal (fun-table-lookup fun (fun-table-fix funtab))
         (fun-table-lookup fun funtab)))

Theorem: fun-table-lookup-fun-table-equiv-congruence-on-funtab

(defthm fun-table-lookup-fun-table-equiv-congruence-on-funtab
  (implies (fun-table-equiv funtab funtab-equiv)
           (equal (fun-table-lookup fun funtab)
                  (fun-table-lookup fun funtab-equiv)))
  :rule-classes :congruence)