		Search-engine friendly clone of the ACL2 documentation.

Exec

Exec-switch-rest

Execute the rest of a switch statement, after evaluating the target.

Signature
(exec-switch-rest cases default target cstate funenv limit) → outcome
Arguments: cases — Guard (swcase-listp cases).; default — Guard (block-optionp default).; target — Guard (valuep target).; cstate — Guard (cstatep cstate).; funenv — Guard (funenvp funenv).; limit — Guard (natp limit).
Returns: outcome — Type (soutcome-resultp outcome).

We go through the cases, until we find a match, in which case we return the result of executing the corresponding block. If we reach the end of the list, we execute the default block, if present. If the default block is absent, we terminate regularly.