		Search-engine friendly clone of the ACL2 documentation.

Static-safety-checking

Check-var

Check if a variable is in a variable table.

Signature
(check-var var varset) → yes/no
Arguments: var — Guard (identifierp var).; varset — Guard (identifier-setp varset).
Returns: yes/no — Type (booleanp yes/no).

Definitions and Theorems

Function: check-var

(defun check-var (var varset)
  (declare (xargs :guard (and (identifierp var)
                              (identifier-setp varset))))
  (let ((__function__ 'check-var))
    (declare (ignorable __function__))
    (in (identifier-fix var)
        (identifier-set-fix varset))))

Theorem: booleanp-of-check-var

(defthm booleanp-of-check-var
  (b* ((yes/no (check-var var varset)))
    (booleanp yes/no))
  :rule-classes :rewrite)

Theorem: check-var-of-identifier-fix-var

(defthm check-var-of-identifier-fix-var
  (equal (check-var (identifier-fix var) varset)
         (check-var var varset)))

Theorem: check-var-identifier-equiv-congruence-on-var

(defthm check-var-identifier-equiv-congruence-on-var
  (implies (identifier-equiv var var-equiv)
           (equal (check-var var varset)
                  (check-var var-equiv varset)))
  :rule-classes :congruence)

Theorem: check-var-of-identifier-set-fix-varset

(defthm check-var-of-identifier-set-fix-varset
  (equal (check-var var (identifier-set-fix varset))
         (check-var var varset)))

Theorem: check-var-identifier-set-equiv-congruence-on-varset

(defthm check-var-identifier-set-equiv-congruence-on-varset
  (implies (identifier-set-equiv varset varset-equiv)
           (equal (check-var var varset)
                  (check-var var varset-equiv)))
  :rule-classes :congruence)