|
|
|---|
|
|
|
|---|
Recognizers of functions in terms.
In translated terms, the `functions' that are applied to argument terms are function symbols and lambda expressions.
The built-in predicates pseudo-termp and termp recognize pseudo-terms and valid translated terms. The following predicates recognize lambda expressions in pseudo-terms and in valid translated terms, as well as functions (in the sense above) in pseudo-terms and in valid translated terms.
Note that the built-in predicate symbolp recognizes functions in pseudo-terms that are not lambda expressions, and that the predicate function-symbolp recognizes functions in valid translated terms that are not lambda expressions (the latter has guard symbolp, so it must be actually preceded by a call of symbolp in guard-verified code). These predicates, with the ones below, provide ways to recognize all kinds of functions in terms.