Top

Defmax-nat

Defmax-nat-implementation

Implementation of defmax-nat.

The implementation functions have formal parameters consistently named as follows:

state is the ACL2 state.
ctx is the context used for errors.
f, y, x1...xn, body, guard, and verify-guards are the honomynous inputs to defmax-nat, where x1...xn is shown as (x1 ... xn) in the documentation. They have no types before being processed, then they acquire types implied by their validation.

Subtopics

Defmax-nat-fn: Process the inputs and generate the event to submit.
Defmax-nat-macro-definition: Definition of the defmax-nat macro.
Defmax-nat-input-processing: Input processing performed by defmax-nat.
Defmax-nat-event-generation: Event generation performed by defmax-nat.