Declare a new variables within the environment.
The newly declare variable is placed in the top scope block.
Function:
(defun declare-var-env (ident env) (declare (xargs :guard (and (identp ident) (envp env)))) (let ((__function__ 'declare-var-env)) (declare (ignorable __function__)) (b* ((env (env-fix env)) ((when (endp env)) nil)) (cons (omap::update (ident-fix ident) nil (first env)) (rest env)))))
Theorem:
(defthm envp-of-declare-var-env (b* ((new-env (declare-var-env ident env))) (envp new-env)) :rule-classes :rewrite)