		Search-engine friendly clone of the ACL2 documentation.

Static-environments

Init-senv

Initialize a static environment.

Signature
(init-senv) → env
Returns: env — Type (senvp env).

The environment is initially empty.

Definitions and Theorems

Function: init-senv

(defun init-senv nil
  (declare (xargs :guard t))
  (let ((__function__ 'init-senv))
    (declare (ignorable __function__))
    (make-senv :identifiers nil)))

Theorem: senvp-of-init-senv

(defthm senvp-of-init-senv
  (b* ((env (init-senv))) (senvp env))
  :rule-classes :rewrite)