Record an existing function as second-order.
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.
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
:defaultnor :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.
A table event that records
This classification is important because defun-inst treats these different kinds of second-order functions differently.