		Search-engine friendly clone of the ACL2 documentation.

Function-environments

Fun-env-extend

Extend a function environment with a function definition.

Signature
(fun-env-extend fundef fenv) → result
Arguments: fundef — Guard (fundefp fundef).; fenv — Guard (fun-envp fenv).
Returns: result — Type (fun-env-resultp result).

If the environment already has a function with the same name, this operation returns an error.

Definitions and Theorems

Function: fun-env-extend

(defun fun-env-extend (fundef fenv)
  (declare (xargs :guard (and (fundefp fundef) (fun-envp fenv))))
  (let ((__function__ 'fun-env-extend))
    (declare (ignorable __function__))
    (b* ((fenv (fun-env-fix fenv))
         ((fundef fundef) fundef)
         (name (fundef->name fundef))
         ((when (fun-env-lookup name fenv))
          (reserrf (list :duplicate-function-definition name)))
         (info (fun-info-from-fundef fundef)))
      (omap::update name info fenv))))

Theorem: fun-env-resultp-of-fun-env-extend

(defthm fun-env-resultp-of-fun-env-extend
  (b* ((result (fun-env-extend fundef fenv)))
    (fun-env-resultp result))
  :rule-classes :rewrite)

Theorem: fun-env-extend-of-fundef-fix-fundef

(defthm fun-env-extend-of-fundef-fix-fundef
  (equal (fun-env-extend (fundef-fix fundef)
                         fenv)
         (fun-env-extend fundef fenv)))

Theorem: fun-env-extend-fundef-equiv-congruence-on-fundef

(defthm fun-env-extend-fundef-equiv-congruence-on-fundef
  (implies (fundef-equiv fundef fundef-equiv)
           (equal (fun-env-extend fundef fenv)
                  (fun-env-extend fundef-equiv fenv)))
  :rule-classes :congruence)

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

(defthm fun-env-extend-of-fun-env-fix-fenv
  (equal (fun-env-extend fundef (fun-env-fix fenv))
         (fun-env-extend fundef fenv)))

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

(defthm fun-env-extend-fun-env-equiv-congruence-on-fenv
  (implies (fun-env-equiv fenv fenv-equiv)
           (equal (fun-env-extend fundef fenv)
                  (fun-env-extend fundef fenv-equiv)))
  :rule-classes :congruence)