		Search-engine friendly clone of the ACL2 documentation.

Defarbrec-table

Defarbrec-infop

Information about a defarbrec call, recorded as a pair's value in the defarbrec table.

(defarbrec-infop x) is a std::defaggregate of the following fields.

call$ — The call of defarbrec, after defarbrec-filter-call.
Invariant (pseudo-event-formp call$).
expansion — The encapsulate generated from the call of defarbrec.
Invariant (pseudo-event-formp expansion).
x1...xn — Formal arguments of the function.
body — Translated unnormalized body of the program-mode function.
update-fns — The names of the generated iterated argument update functions.
Invariant (symbol-listp update-fns).
terminates-fn — The name of the generated termination testing predicate.
Invariant (symbolp terminates-fn).
measure-fn — The name of the generated measure function.
Invariant (symbolp measure-fn).

Source link: defarbrec-infop

The name of the generated recursive logic-mode function is the key of the pair in the table.

The call of defarbrec is stored without any :print and :show-only options because, as explained in the documentation, redundancy checking ignores those options.

Subtopics

Defarbrec-info: Raw constructor for defarbrec-infop structures.
Make-defarbrec-info: Constructor macro for defarbrec-infop structures.
Change-defarbrec-info: A copying macro that lets you create new defarbrec-infop structures, based on existing structures.
Honsed-defarbrec-info: Raw constructor for honsed defarbrec-infop structures.
Make-honsed-defarbrec-info: Constructor macro for honsed defarbrec-infop structures.
Defarbrec-info->x1...xn: Access the x1...xn field of a defarbrec-infop structure.
Defarbrec-info->update-fns: Access the update-fns field of a defarbrec-infop structure.
Defarbrec-info->terminates-fn: Access the terminates-fn field of a defarbrec-infop structure.
Defarbrec-info->measure-fn: Access the measure-fn field of a defarbrec-infop structure.
Defarbrec-info->expansion: Access the expansion field of a defarbrec-infop structure.
Defarbrec-info->call$: Access the call$ field of a defarbrec-infop structure.
Defarbrec-info->body: Access the body field of a defarbrec-infop structure.