|
|
|---|
|
|
|
|---|
Updates to SOFT since the ACL2-2015 Workshop.
Nullary function variables (i.e. function variables with arity 0) are now allowed.
For second-order functions and theorems
that depend on two or more function variables,
the Workshop paper suggests to use underscores
to separate the function variables inside the square brackets,
e.g.
The defun2, defchoose2, defun-sk2, and defun-inst macros no longer include an explicit list of function parameters. The function is implicitly parameterized over the function variables that it depends on. This simplifies the implementation. It also avoids the repetition of the function variables when using the naming convention of including, in the name of a second-order function, the function variables that it depends on (enclosed in square brackets).