Notion of definedness of functions, for some event macros.
As far as certain event macros are concerned,
an ACL2 named function is defined if and only if
it has a non-
The unnormalized body of a named function is
A valid untranslated term never translates to
However, the built-in program-mode functions are defined but do not have an unnormalized body. Thus, the event macros that use this notion of definedness would not regard these functions as being defined. This is only an issue for program-mode functions, not for logic-mode functions (including the built-in ones); thus, if an event macro requires a function (e.g. to be transformed) to be in logic mode and to be defined, checking the unnormalized body is an accurate way to establish if the logic-mode function is defined.
The system utility ubody (or ubody+) retrieves the unnormalized body of a function. It is a specialization of the built-in body system utility, which retrieves the unnormalized or normalized body of a function. based on the flag passed as argument. The normalized body of a function may differ from the unnormalized one because the former may be obtained from the latter via some simplifications.