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.

DropData

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