		Search-engine friendly clone of the ACL2 documentation.

Function-environments

Fun-env-lookup

Look up a function in an environment by name.

Signature
(fun-env-lookup name fenv) → info?
Arguments: name — Guard (identp name).; fenv — Guard (fun-envp fenv).
Returns: info? — Type (fun-info-optionp info?).

Definitions and Theorems

Function: fun-env-lookup

(defun fun-env-lookup (name fenv)
  (declare (xargs :guard (and (identp name) (fun-envp fenv))))
  (let ((__function__ 'fun-env-lookup))
    (declare (ignorable __function__))
    (cdr (omap::assoc (ident-fix name)
                      (fun-env-fix fenv)))))

Theorem: fun-info-optionp-of-fun-env-lookup

(defthm fun-info-optionp-of-fun-env-lookup
  (b* ((info? (fun-env-lookup name fenv)))
    (fun-info-optionp info?))
  :rule-classes :rewrite)

Theorem: fun-env-lookup-of-ident-fix-name

(defthm fun-env-lookup-of-ident-fix-name
  (equal (fun-env-lookup (ident-fix name) fenv)
         (fun-env-lookup name fenv)))

Theorem: fun-env-lookup-ident-equiv-congruence-on-name

(defthm fun-env-lookup-ident-equiv-congruence-on-name
  (implies (ident-equiv name name-equiv)
           (equal (fun-env-lookup name fenv)
                  (fun-env-lookup name-equiv fenv)))
  :rule-classes :congruence)

Theorem: fun-env-lookup-of-fun-env-fix-fenv

(defthm fun-env-lookup-of-fun-env-fix-fenv
  (equal (fun-env-lookup name (fun-env-fix fenv))
         (fun-env-lookup name fenv)))

Theorem: fun-env-lookup-fun-env-equiv-congruence-on-fenv

(defthm fun-env-lookup-fun-env-equiv-congruence-on-fenv
  (implies (fun-env-equiv fenv fenv-equiv)
           (equal (fun-env-lookup name fenv)
                  (fun-env-lookup name fenv-equiv)))
  :rule-classes :congruence)