# Outcome

Fixtype of Syntheto outcomes.

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

##### Member Tags → Types

`:function-success` → outcome-function-success
`:type-success` → outcome-type-success
`:specification-success` → outcome-specification-success
`:theorem-success` → outcome-theorem-success
`:transformation-success` → outcome-transformation-success
`:proof-obligation-failure` → outcome-proof-obligation-failure
`:theorem-failure` → outcome-theorem-failure
`:transformation-failure` → outcome-transformation-failure
`:unexpected-failure` → outcome-unexpected-failure

Each type of top-level definition, when submitted to ACL2,
will be accepted or rejected. The success or failure
of the submission is modeled by an outcome, which is returned
to the submitter.

A function or clique of mutually-recursive functions, when
submitted successfully to ACL2, is represented by function-success.
Similarly, a type definition or clique of mutually-recursive type
definitions is represented by type-success. Specifications,
theorems, and transformations also have success types.

Since a successful transformation results in new submitted top-level
definitions, those are returned as part of the success outcome.

For submission of a top-level definition to be accepted,
there are certain implicit proof obligations such as termination and
guard verification. If one of these fails, a
proof-obligation-failure outcome is returned, containing
an expression that could not be proved. This failure may result for a
number of different reasons, and may result from a number of different
top-level constructs including failure to prove the applicability
condition of a transformation.

If a theorem is submitted that is not mechanically proved by ACL2,
a theorem-failure outcome is returned.

If a transformation is submitted that is applicable, but fails
due to some other reason, potentially a transformation-failure
outcome is returned.

Any other submission failure results in a unexpected-failure
outcome, which might have been expected but is at least not otherwise
classified.

### Subtopics

- Outcome-fix
- Fixing function for outcome structures.
- Outcome-case
- Case macro for the different kinds of outcome structures.
- Outcomep
- Recognizer for outcome structures.
- Outcome-equiv
- Basic equivalence relation for outcome structures.
- Outcome-proof-obligation-failure
- Outcome-transformation-success
- Outcome-kind
- Get the
*kind* (tag) of a outcome structure. - Outcome-unexpected-failure
- Outcome-type-success
- Outcome-transformation-failure
- Outcome-theorem-success
- Outcome-theorem-failure
- Outcome-specification-success
- Outcome-function-success