Module build

Source
Expand description

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 ๐Ÿ”’