Module resolution

Trait resolution: given a trait reference, we track which local clause caused it to be true. This module is independent from the rest of hax, in particular it doesn’t use its state-tracking machinery.

Structs

• AnnotatedTraitPred
• Candidate 🔒
  A candidate projects self along a path reaching some predicate. A candidate is selected when its predicate is the one expected, aka target.
• ImplExpr
• PredicateSearcher
  Stores a set of predicates along with where they came from.

Enums

• BoundPredicateOrigin
  Items have various predicates in scope. path_to uses them as a starting point for trait resolution. This tracks where each of them comes from.
• ImplExprAtom
• PathChunk

Functions

• initial_search_predicates 🔒
  The predicates to use as a starting point for resolving trait references within this item. This includes the “self” predicate if applicable and the required_predicates of this item and all its parents, numbered starting from the parents.
• parents_trait_predicates 🔒
• shallow_resolve_trait_ref
  Attempts to resolve an obligation to an ImplSource. The result is a shallow ImplSource resolution, meaning that we do not resolve all nested obligations on the impl. Note that type check should guarantee to us that all nested obligations could be resolved if we wanted to.

Type Aliases

• Path