		Search-engine friendly clone of the ACL2 documentation.

Dynamic-function-environments

Init-function-denv

Initial dynamic function environment.

Signature
(init-function-denv) → env
Returns: env — Type (function-denvp env).

This is empty.

Definitions and Theorems

Function: init-function-denv

(defun init-function-denv nil
  (declare (xargs :guard t))
  (let ((__function__ 'init-function-denv))
    (declare (ignorable __function__))
    nil))

Theorem: function-denvp-of-init-function-denv

(defthm function-denvp-of-init-function-denv
  (b* ((env (init-function-denv)))
    (function-denvp env))
  :rule-classes :rewrite)