Module hax_frontend_exporter::traits
source · Re-exports§
pub use utils::erase_and_norm;
pub use resolution::PredicateSearcher;
Modules§
- 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 🔒
Structs§
- 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 ofClone
for(A, B)
with the concrete implementations foru8
and&str
, represented as a tree.
Enums§
- The source of a particular trait implementation. Most often this is either
Concrete
for a concreteimpl Trait for Type {}
item, orLocalBound
for a context-boundwhere T: Trait
.
Functions§
- Retrieve the
Self: Trait
clause for a trait associated item. - Solve the trait obligations for a specific item use (for example, a method call, an ADT, etc.).
- This is the entrypoint of the solving.
- Given a clause
clause
in the context of some impl blockimpl_did
, susbts correctlySelf
fromclause
and (1) derive aClause
and (2) resolve anImplExpr
.