Check if a variable is in a list of scopes.
(var-in-scopes-p var scopes) → yes/no
This is an auxiliary function, used by others below.
Function:
(defun var-in-scopes-p (var scopes) (declare (xargs :guard (and (identp var) (scope-listp scopes)))) (let ((__function__ 'var-in-scopes-p)) (declare (ignorable __function__)) (b* (((when (endp scopes)) nil) (var-val (omap::assoc (ident-fix var) (scope-fix (car scopes)))) ((when (consp var-val)) t)) (var-in-scopes-p var (cdr scopes)))))
Theorem:
(defthm booleanp-of-var-in-scopes-p (b* ((yes/no (var-in-scopes-p var scopes))) (booleanp yes/no)) :rule-classes :rewrite)
Theorem:
(defthm var-in-scopes-p-when-valuep-of-read-auto-var-aux (implies (valuep (read-auto-var-aux var scopes)) (var-in-scopes-p var scopes)))
Theorem:
(defthm var-in-scopes-p-when-read-auto-var-aux (implies (read-auto-var-aux var scopes) (var-in-scopes-p var scopes)))
Theorem:
(defthm not-var-in-scopes-p-when-not-read-auto-var-aux (implies (not (read-auto-var-aux var scopes)) (not (var-in-scopes-p var scopes))))
Theorem:
(defthm var-in-scopes-p-of-ident-fix-var (equal (var-in-scopes-p (ident-fix var) scopes) (var-in-scopes-p var scopes)))
Theorem:
(defthm var-in-scopes-p-ident-equiv-congruence-on-var (implies (ident-equiv var var-equiv) (equal (var-in-scopes-p var scopes) (var-in-scopes-p var-equiv scopes))) :rule-classes :congruence)
Theorem:
(defthm var-in-scopes-p-of-scope-list-fix-scopes (equal (var-in-scopes-p var (scope-list-fix scopes)) (var-in-scopes-p var scopes)))
Theorem:
(defthm var-in-scopes-p-scope-list-equiv-congruence-on-scopes (implies (scope-list-equiv scopes scopes-equiv) (equal (var-in-scopes-p var scopes) (var-in-scopes-p var scopes-equiv))) :rule-classes :congruence)