## 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.