		Search-engine friendly clone of the ACL2 documentation.

Write-env

Overwrite the value of a variable.

Signature
(write-env ident value? env) → new-env
Arguments: ident — Guard (identp ident).; value? — Guard (c::value-optionp value?).; env — Guard (envp env).
Returns: new-env — Type (envp new-env).

This assumes that the variable is already declared (see declare-var-env). If the variable has been shadowed, only the unshadowed variable is overwritten.

Definitions and Theorems

Function: write-env

(defun write-env (ident value? env)
  (declare (xargs :guard (and (identp ident)
                              (c::value-optionp value?)
                              (envp env))))
  (let ((__function__ 'write-env))
    (declare (ignorable __function__))
    (b* ((env (env-fix env))
         (value? (c::value-option-fix value?))
         ((when (endp env)) nil)
         (lookup (omap::assoc ident (first env))))
      (if lookup (cons (omap::update ident value? (first env))
                       (rest env))
        (cons (first env)
              (write-env ident value? (rest env)))))))

Theorem: envp-of-write-env

(defthm envp-of-write-env
  (b* ((new-env (write-env ident value? env)))
    (envp new-env))
  :rule-classes :rewrite)