		Search-engine friendly clone of the ACL2 documentation.

Std/system

Std/system/function-queries

Utilities to query functions.

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

Subtopics

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, or nil 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.