Look up a tag in a tag environment.
(tag-env-lookup tag env) → info
Function:
(defun tag-env-lookup (tag env) (declare (xargs :guard (and (identp tag) (tag-envp env)))) (let ((__function__ 'tag-env-lookup)) (declare (ignorable __function__)) (cdr (omap::assoc (ident-fix tag) (tag-env-fix env)))))
Theorem:
(defthm tag-info-optionp-of-tag-env-lookup (b* ((info (tag-env-lookup tag env))) (tag-info-optionp info)) :rule-classes :rewrite)
Theorem:
(defthm tag-env-lookup-of-ident-fix-tag (equal (tag-env-lookup (ident-fix tag) env) (tag-env-lookup tag env)))
Theorem:
(defthm tag-env-lookup-ident-equiv-congruence-on-tag (implies (ident-equiv tag tag-equiv) (equal (tag-env-lookup tag env) (tag-env-lookup tag-equiv env))) :rule-classes :congruence)
Theorem:
(defthm tag-env-lookup-of-tag-env-fix-env (equal (tag-env-lookup tag (tag-env-fix env)) (tag-env-lookup tag env)))
Theorem:
(defthm tag-env-lookup-tag-env-equiv-congruence-on-env (implies (tag-env-equiv env env-equiv) (equal (tag-env-lookup tag env) (tag-env-lookup tag env-equiv))) :rule-classes :congruence)