Module traits

Re-exports

• pub use utils::erase_and_norm;
• pub use utils::implied_predicates;
• pub use utils::predicates_defined_on;
• pub use utils::required_predicates;
• pub use utils::self_predicate;
• pub use resolution::PredicateSearcher;

Modules

• 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.
• utils 🔒
  Each item can involve three kinds of predicates:

Structs

• ImplExpr
  An ImplExpr describes the full data of a trait implementation. Because of generics, this may need to combine several concrete trait implementation items. For example, ((1u8, 2u8), "hello").clone() combines the generic implementation of Clone for (A, B) with the concrete implementations for u8 and &str, represented as a tree.

Enums

• ImplExprAtom
  The source of a particular trait implementation. Most often this is either Concrete for a concrete impl Trait for Type {} item, or LocalBound for a context-bound where T: Trait.
• ImplExprPathChunk

Functions

• self_clause_for_item
  Retrieve the Self: Trait clause for a trait associated item.
• solve_item_implied_traits
  Solve the trait obligations for implementing a trait (or for trait associated type bounds) in the current context.
• solve_item_required_traits
  Solve the trait obligations for a specific item use (for example, a method call, an ADT, etc.) in the current context.
• solve_item_traits_inner 🔒
  Apply the given generics to the provided clauses and resolve the trait references in the current context.
• solve_trait
  This is the entrypoint of the solving.
• super_clause_to_clause_and_impl_expr
  Given a clause clause in the context of some impl block impl_did, susbts correctly Self from clause and (1) derive a Clause and (2) resolve an ImplExpr.