		Search-engine friendly clone of the ACL2 documentation.

Static-safety-checking

Add-var

Add a variable to a variable table.

Signature
(add-var var varset) → varset?
Arguments: var — Guard (identifierp var).; varset — Guard (identifier-setp varset).
Returns: varset? — Type (identifier-set-resultp varset?).

If a variable with the same name is already in the table, an error is returned.

If this function does not return an error, it is equivalent to insert.

Definitions and Theorems

Function: add-var

(defun add-var (var varset)
  (declare (xargs :guard (and (identifierp var)
                              (identifier-setp varset))))
  (let ((__function__ 'add-var))
    (declare (ignorable __function__))
    (b* ((var (identifier-fix var))
         (varset (identifier-set-fix varset)))
      (if (in var varset)
          (reserrf (list :duplicate-variable var))
        (insert var varset)))))

Theorem: identifier-set-resultp-of-add-var

(defthm identifier-set-resultp-of-add-var
  (b* ((varset? (add-var var varset)))
    (identifier-set-resultp varset?))
  :rule-classes :rewrite)

Theorem: add-var-to-set-insert

(defthm add-var-to-set-insert
  (b* ((varset1 (add-var var varset)))
    (implies (not (reserrp varset1))
             (equal varset1
                    (insert (identifier-fix var)
                            (identifier-set-fix varset))))))

Theorem: add-var-of-identifier-fix-var

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

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

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

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

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

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

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