# Second-order-function-instances

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
instantiation,
which is applied to the body, measure (if recursive), and guard
of the second-order function.

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 functional
instance of the
termination theorem
of the second-order function that is being instantiated.

### Naming Conventions

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.

### Subtopics

- Defun-inst
- Introduce a function by instantiating a second-order functions.