		Search-engine friendly clone of the ACL2 documentation.

Functional-instantiation

Functional-instantiation-in-ACL2r

Additional requirements for :functional-instance hints in ACL2(r)

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.