FUNCTIONAL-INSTANTIATION-IN-ACL2R

additional requirements for :functional-instance hints in ACL2(r)
Major Section:  MISCELLANEOUS

This documentation topic relates to ACL2(r), the modification of ACL2 that supports the real numbers (see real).

See hints and see lemma-instance for a discussion of :use hints that employ the :functional-instance keyword. Here, we document additional requirements for such hints that applies to ACL2(r). We assume familiarity with lemma instances; see lemma-instance.

(1) When functionally instantiating a non-classical formula, it is illegal to use pseudo-lambda expressions in a lemma instance.

(2) A classical function symbol must be bound either to a classical function symbol or to a lambda (or, if allowed, pseudo-lambda) expression with a classical body. Similarly, a non-classical function symbol must be bound either to a non-classical function symbol or to a lambda (or, if allowed, pseudo-lambda) expression with a non-classical body.