Module build

Building proof trees incrementally during trait solving.

This code is a bit of a mess and can hopefully be mostly ignored. For a general overview of how it works, see the comment on ProofTreeBuilder.

Structs

ProofTreeBuilder 🔒

The core data structure when building proof trees.

WipCanonicalGoalEvaluation 🔒

WipCanonicalGoalEvaluationStep 🔒

This only exists during proof tree building and does not have a corresponding struct in inspect. We need this to track a bunch of metadata about the current evaluation.

WipGoalEvaluation 🔒

WipProbe 🔒

Enums

DebugSolver 🔒

The current state of the proof tree builder, at most places in the code, only one or two variants are actually possible.

WipProbeStep 🔒