		Search-engine friendly clone of the ACL2 documentation.

Vl-assertion

Representation of an immediate assertion.

This is a product type introduced by defprod.

name — maybe-string: The label for this assertion, if provided. Note that in a statement context, labels like foo : assert ... mainly get turned into named begin/end blocks, but we do take care to also put the name into the assertion object.
type — vl-asserttype-p: The type of this assertion, e.g., assert, assume, etc.
deferral — vl-assertdeferral-p: Indicates whether this assertion is a regular, non-deferred assertion, or a #0 or final deferred assertion.
condition — vl-expr: The condition to assert. Note that since this is an immediate assertion, the condition is a simple expression, not a fancy sequence or property.
success — vl-stmt: For most assertions, this is the success statement for the associated action block, or a vl-nullstmt if there is no success statement. Note that cover assertions are special and don't have an action block, so for a cover assertion this is just the associated statement, if any.
failure — vl-stmt: This is the else statement from the action block, or a vl-nullstmt if there is no else statement. For cover assertions this is always just a vl-nullstmt since there is no else action.
loc — vl-location: Location of this statement in the source code.