		Search-engine friendly clone of the ACL2 documentation.

Read-env

Retrieve the value of a variable.

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

A result of nil indicates that the variable is not in scope (see in-scope-env), or its value is unknown.

Definitions and Theorems

Function: read-env

(defun read-env (ident env)
  (declare (xargs :guard (and (identp ident) (envp env))))
  (let ((__function__ 'read-env))
    (declare (ignorable __function__))
    (b* (((when (endp env)) nil)
         (lookup (omap::assoc ident (env-block-fix (first env)))))
      (if lookup (cdr lookup)
        (read-env ident (rest env))))))

Theorem: value-optionp-of-read-env

(defthm value-optionp-of-read-env
  (b* ((value? (read-env ident env)))
    (c::value-optionp value?))
  :rule-classes :rewrite)