Expand description
Data types for the path-refinement layer.
These structures are produced by the backward visitor and consumed by the
forward visitor, engine, and diagnostic formatting. ContractFact is the
only variant never produced by the backward visitor itself — it is injected
by the engine before the forward visit.
Structs§
- Relevant
MirItems - MIR items relevant to one
(checkpoint, path, property)item.
Enums§
- Backward
Item - One item kept while walking a path backward.
- Forget
Reason - Reason for conservatively forgetting relevant state.
- Keep
Reason - Why a retained item is relevant.