		Search-engine friendly clone of the ACL2 documentation.

Evaluation

Exec-outcome

Fixtype of execution outcomes.

This is a tagged union type, introduced by fty::deftagsum.

Member Tags → Types

:terminating → exec-outcome-terminating
:error → exec-outcome-error
:nonterminating → exec-outcome-nonterminating

When attempting to exhaustively perform execution steps, there are three possible outcomes: (i) a final state is reached, with a final result value; (ii) an error state is reached; and (iii) execution continues forever. Here we capture these possible outcomes.

Subtopics

Exec-outcome-case: Case macro for the different kinds of exec-outcome structures.
Exec-outcome-fix: Fixing function for exec-outcome structures.
Exec-outcome-equiv: Basic equivalence relation for exec-outcome structures.
Exec-outcome-p: Recognizer for exec-outcome structures.
Exec-outcome-terminating
Exec-outcome-nonterminating
Exec-outcome-kind: Get the kind (tag) of a exec-outcome structure.
Exec-outcome-error