		Search-engine friendly clone of the ACL2 documentation.

Defun-inst-implementation

Implementation of defun-inst.

Defun-inst-quant-events: Generate a list of events to submit, when instantiating a quantifier second-order function.
Defun-inst-plain-events: Generate a list of events to submit, when instantiating a plain second-order function.
Defun-inst-fn: Validate some of the inputs to defun-inst and generate the event form to submit.
Defun-inst-choice-events: Generate a list of events to submit, when instantiating a choice second-order function.
Check-qrewrite-rule-funvars: Check if the rewrite rule of a quantifier second-order function, or of an instance of it, depends exactly on the same function variables that the matrix of the function depends on.
Check-sofun-inst: Recognize designations of instances of second-order functions.
Show-defun-inst: Show the event form generated by defun-inst, without submitting them.
Defun-inst-macro-definition: Definition of the defun-inst macro.