Function-variables
Notion of function variable.
A function variable is an uninterpreted ACL2 function
introduced via defunvar.
This macro specifies the arity of the function variable.
A function variable is used in
second-order functions and
second-order theorems
as a placeholder for any function with the same arity.
Naming Conventions
Starting function variable names with ?,
as in the examples in the SOFT documentation pages,
provides a visual cue for their function variable status.
However, SOFT does not enforce this naming convention.
Subtopics
- Defunvar
- Introduce a function variable.
