Modules§
- canonical 🔒
- Canonicalization is used to separate some goal from its context, throwing away unnecessary information in the process.
- probe 🔒
Structs§
- Eval
Ctxt - Nested
Goals 🔒 - Replace
Alias 🔒With Infer - Eagerly replace aliases with inference variables, emitting
AliasRelategoals, used when adding goals to theEvalCtxt. We compute theAliasRelategoals before evaluating the actual goal to get all the constraints we can.
Enums§
- Current
Goal 🔒Kind - The kind of goal we’re currently proving.
- Generate
Proof Tree