		Search-engine friendly clone of the ACL2 documentation.

Jexpr-methods

Method names in a Java expression.

We return all the method names in method calls.

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

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

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

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