:functional-instancehints 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
: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.