Modules§
- analyse 🔒
- An infrastructure to mechanically analyse proof trees.
Structs§
- Canonical
Goal Evaluation - Goal
Evaluation - When evaluating a goal we also store the original values
for the
CanonicalVarValuesof the canonicalized goal. We use this to map any CanonicalState from the localInferCtxtof the solver query to theInferCtxtof the caller. - Inspect
Candidate - Inspect
Config - Inspect
Goal - Probe
- A self-contained computation during trait solving. This either
corresponds to a
EvalCtxt::probe(_X)call or the root evaluation of a goal. - State
- Some
datatogether with information about how they relate to the input of the canonical query.
Enums§
- Canonical
Goal Evaluation Kind - Probe
Kind - What kind of probe we’re in. In case the probe represents a candidate, or the final result of the current goal - via ProbeKind::Root - we also store the QueryResult.
- Probe
Step
Traits§
- Proof
Tree Infer Ctxt Ext - Proof
Tree Visitor - The public API to interact with proof trees.