		Search-engine friendly clone of the ACL2 documentation.

Flattening

Fenv-const-lookup

Look up a constant in a flattening environment.

Signature
(fenv-const-lookup const env) → val
Arguments: const — Guard (identifierp const).; env — Guard (fenvp env).
Returns: val — Type (value-optionp val).

We return the associated value if the constant is found in the constant flattening environment of the flattening environment. Otherwise we return nil.

Definitions and Theorems

Function: fenv-const-lookup

(defun fenv-const-lookup (const env)
  (declare (xargs :guard (and (identifierp const) (fenvp env))))
  (let ((__function__ 'fenv-const-lookup))
    (declare (ignorable __function__))
    (cdr (omap::assoc (identifier-fix const)
                      (fenv->constants env)))))

Theorem: value-optionp-of-fenv-const-lookup

(defthm value-optionp-of-fenv-const-lookup
  (b* ((val (fenv-const-lookup const env)))
    (value-optionp val))
  :rule-classes :rewrite)

Theorem: fenv-const-lookup-of-identifier-fix-const

(defthm fenv-const-lookup-of-identifier-fix-const
  (equal (fenv-const-lookup (identifier-fix const)
                            env)
         (fenv-const-lookup const env)))

Theorem: fenv-const-lookup-identifier-equiv-congruence-on-const

(defthm fenv-const-lookup-identifier-equiv-congruence-on-const
  (implies (identifier-equiv const const-equiv)
           (equal (fenv-const-lookup const env)
                  (fenv-const-lookup const-equiv env)))
  :rule-classes :congruence)

Theorem: fenv-const-lookup-of-fenv-fix-env

(defthm fenv-const-lookup-of-fenv-fix-env
  (equal (fenv-const-lookup const (fenv-fix env))
         (fenv-const-lookup const env)))

Theorem: fenv-const-lookup-fenv-equiv-congruence-on-env

(defthm fenv-const-lookup-fenv-equiv-congruence-on-env
  (implies (fenv-equiv env env-equiv)
           (equal (fenv-const-lookup const env)
                  (fenv-const-lookup const env-equiv)))
  :rule-classes :congruence)