		Search-engine friendly clone of the ACL2 documentation.

Jexpr-vars

Variables in a Java expression.

We return all the names in expression names. The list is without duplicates but in no particular order.

Theorem: return-type-of-jexpr-vars.vars

(defthm return-type-of-jexpr-vars.vars
  (b* ((?vars (jexpr-vars expr)))
    (string-listp vars))
  :rule-classes :rewrite)

Theorem: return-type-of-jexpr-list-vars.vars

(defthm return-type-of-jexpr-list-vars.vars
  (b* ((?vars (jexpr-list-vars exprs)))
    (string-listp vars))
  :rule-classes :rewrite)