|
|
|---|
|
|
|
|---|
Notion of instance of a second-order function.
An instance of a second-order function is an ACL2 function
introduced via defun-inst,
which replaces function variables that the second-order function depends on
with functions with matching arities.
This macro specifies the replacement as an
The new function is second-order if it still depends on function variables,
otherwise it is first-order.
The new function is recursive iff
the second-order function that is being instantiated is recursive;
in this case,
defun-inst generates a termination proof for the new function
that uses a
If the name of the second-order function that is being instantiated follows the naming convention described in second-order-functions, the name of the instance can be obtained by replacing the names of the function variables between square brackets with the names of the replacing functions in the instantiation, as in the examples in the SOFT documentation pages, This conveys the idea of applying the second-order function to the functions that replace the function variables. However, SOFT does not enforce this naming convention.