Top

Semantics-deeply-embedded

Proof-outcome

Fixtype of semantic proof outcomes.

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

Member Tags → Types

:assertion → proof-outcome-assertion
:fail → proof-outcome-fail
:error → proof-outcome-error

These are the possible results of executing a proof tree:

The proof tree provides a valid proof of an assertion.
The proof fails to prove any assertion.
The proof causes an error during execution

See exec-proof-tree.

Subtopics

Proof-outcome-fix: Fixing function for proof-outcome structures.
Proof-outcome-case: Case macro for the different kinds of proof-outcome structures.
Proof-outcome-equiv: Basic equivalence relation for proof-outcome structures.
Proof-outcomep: Recognizer for proof-outcome structures.
Proof-outcome-assertion
Proof-outcome-kind: Get the kind (tag) of a proof-outcome structure.
Proof-outcome-fail
Proof-outcome-error