		Search-engine friendly clone of the ACL2 documentation.

Svex-vars

Svex-vars-basics

Very basic rules about svex-vars

Definitions and Theorems

Theorem: svex-vars-when-quote

(defthm svex-vars-when-quote
  (implies (equal (svex-kind x) :quote)
           (equal (svex-vars x) nil))
  :rule-classes ((:rewrite :backchain-limit-lst 0)))

Theorem: svex-vars-when-var

(defthm svex-vars-when-var
  (implies (equal (svex-kind x) :var)
           (equal (svex-vars x)
                  (list (svex-var->name x))))
  :rule-classes ((:rewrite :backchain-limit-lst 0)))

Theorem: svex-vars-when-call

(defthm svex-vars-when-call
  (implies (equal (svex-kind x) :call)
           (equal (svex-vars x)
                  (svexlist-vars (svex-call->args x))))
  :rule-classes ((:rewrite :backchain-limit-lst 0)))

Theorem: svex-vars-of-svex-quote

(defthm svex-vars-of-svex-quote
  (equal (svex-vars (svex-quote val))
         nil))

Theorem: svex-vars-of-svex-var

(defthm svex-vars-of-svex-var
  (equal (svex-vars (svex-var name))
         (list (svar-fix name))))

Theorem: svex-vars-of-svex-call

(defthm svex-vars-of-svex-call
  (equal (svex-vars (svex-call fn args))
         (svexlist-vars args)))