Second-order-functions
Notion of second-order function.
A second-order function is an ACL2 function
that depends on
one or more function variables
and that is explicitly recorded via defsoft.
The function variables that the second-order function depends on
may be replaced by functions of matching arities,
obtaining a new function that is an
instance
of the second-order function.
Naming Conventions
Ending second-order function names
with the function variables it depends on (in any order),
enclosed in square brackets,
as in the examples in the SOFT documentation pages,
conveys the dependency on the function variables
and provides a visual cue for their implicit presence.
However, SOFT does not enforce this naming convention.
Subtopics
- Defsoft
- Record an existing function as second-order.
- Defun2
- Introduce a second-order function
via a second-order version of defun.
- Defun-sk2
- Introduce a second-order function
via a second-order version of defun-sk.
- Defchoose2
- Introduce a second-order function
via a second-order version of defchoose.
- Define-sk2
- Introduce a second-order function
via a second-order version of std::define-sk.
- Defund-sk2
- Introduce a second-order function
via a second-order version of ACL2::defund-sk.
- Define2
- Introduce a second-order function
via a second-order version of define.
- Defund2
- Introduce a second-order function
via a second-order version of defund.
