Utilities to query functions.

These utilities are mostly for named functions in the world, but some utilities also work on lambda expressions.

- Defun-sk-queries
- Utilities to query
`defun-sk`functions. - Tail-recursive-p
- Check if a singly recursive function is tail-recursive.
- Termination-theorem$
- A logic-mode guard-verified version of
the built-in
termination-theorem . - Measure
- Measure expression of a named logic-mode recursive function.
- Arity+
- Enhanced variant of
`arity`. - Unwrapped-nonexec-body+
- Enhanced variant of
`unwrapped-nonexec-body`. - Ubody
- Unnormalized body of a named function, or body of a lambda expression.
- Ruler-extenders+
- Enhanced variant of
`ruler-extenders`. - Recursive-calls
- Recursive calls of a named non-mutually-recursive function, along with the controlling tests.
- Guard-theorem-no-simplify$
- A logic-mode guard-verified version of
`guard-theorem-no-simplify`. - Well-founded-relation+
- Enhanced variant of
`well-founded-relation`. - Unwrapped-nonexec-body
- Body of a non-executable defined named function, without the ``non-executable wrapper''.
- Measured-subset+
- Enhanced variant of
`measured-subset`. - Measure+
- Enhanced variant of
`measure`. - Ruler-extenders
- Ruler-extenders of a named logic-mode recursive function.
- Number-of-results+
- Enhanced variant of
`number-of-results`. - Induction-machine+
- Enhanced variant of
`induction-machine`. - Non-executablep+
- Enhanced variant of
`non-executablep`. - Pure-raw-p
- Check if a function has raw Lisp code and is pure, i.e. it has no side effects.
- Irecursivep+
- Enhanced variant of
`irecursivep`. - Formals+
- Enhanced variant of
`formals`. - Stobjs-out+
- Enhanced variant of
`stobjs-out`. - Induction-machine
- Induction machine of a named logic-mode (singly) recursive function.
- Definedp+
- Enhanced variant of
`definedp`. - Number-of-results
- Number of values returned by a named function.
- Ubody+
- Enhanced variant of
`ubody`. - Guard-theorem-no-simplify
- A version of
`guard-theorem`that does no simplification. - Uguard
- Unoptimized guard of a named function or of a lambda expression.
- Rawp
- Check if a named function has raw Lisp code.
- Irecursivep
- List of mutually recursive functions of which
the specified named function is a member,
based on the
`defun`form that introduced this function, ornil if the specified function is not recursive. - Defchoose-queries
- Utilities to query
`defchoose`functions. - Uguard+
- Enhanced variant of
`uguard`. - Stobjs-in+
- Enhanced variant of
`stobjs-in`. - No-stobjs-p+
- Enhanced variant of
`no-stobjs-p`. - Well-founded-relation
- Well-founded relation of a named logic-mode recursive function.
- Definedp
- Check if a named logic-mode function is defined.
- Primitivep+
- Enhanced variant of
`primitivep`. - Guard-verified-p+
- Enhanced variant of
`guard-verified-p`. - No-stobjs-p
- Check if a named function has no input or output stobjs.
- Measured-subset
- Subset of the formal arguments of a named logic-mode recursive function that occur in its measure expression.
- Guard-verified-p
- Check if a named function or theorem is
`guard`-verified. - Primitivep
- Check if a named function is primitive.
- Non-executablep
- Non-executable status of a named function.
- Fundef-enabledp
- Check if the definition of a named function is enabled.
- Fundef-disabledp
- Check if the definition of a named function is disabled.
- Ibody
- Retrieve the untranslated body of a function.
- Std/system/arity
- Theorems about
`arity`.