Top

Defmin-int

Defmin-int-implementation

Implementation of defmin-int.

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 defmin-int, 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

Defmin-int-fn: Process the inputs and generate the event to submit.
Defmin-int-macro-definition: Definition of the defmin-int macro.
Defmin-int-input-processing: Input processing performed by defmin-int.
Defmin-int-event-generation: Event generation performed by defmin-int.