		Search-engine friendly clone of the ACL2 documentation.

Defsoft

Record an existing function as second-order.

General Form

(defsoft sofun)

Inputs

sofun

A symbol, which must name an existing ACL2 function that was introduced, at the lowest level, via defun or defchoose. The user may have used a higher-level event macro, such as define or defun-sk, but such macros eventually reduce to primitive ones like defun.
The function must depend on at least one function variables.
If the function is recursive, its well-founded relation must be o<.
If the function is introduced (directly or indirectly) via a defun-sk with a universal quantifier and a custom rewrite rule (i.e. neither :default nor :direct), the function variables that (the formula of) the custom rule depends on must be the same as the ones that the body of the function depends on.

Generated Events

A table event that records sofun as a second-order function, along with the function variables that it depends on.

Classification

If sofun is introduced via defchoose, it is called a `choice' second-order function.

Otherwise, sofun is introduced via defun (see constraints above), and there are two cases.

If sofun is introduced via defun-sk (which expands to defun, but it leaves a record in the ACL2 world), it is called a `quantifier' second-order function.

Otherwise, sofun is called a `plain' second-order function.

This classification is important because defun-inst treats these different kinds of second-order functions differently.

Related Macros

While defsoft may be useful to make a function second-order after the fact, one may often use macros like defun2, which combine non-SOFT macros like defun with defsoft.

Subtopics

Defsoft-implementation: Implementation of defsoft.