Expand description
An infrastructure to mechanically analyse proof trees.
It is unavoidable that this representation is somewhat lossy as it should hide quite a few semantically relevant things, e.g. canonicalization and the order of nested goals.
@lcnr: However, a lot of the weirdness here is not strictly necessary and could be improved in the future. This is mostly good enough for coherence right now and was annoying to implement, so I am leaving it as is until we start using it for something else.
Re-exports§
use std::assert_matches;🔒use rustc_infer::infer::InferCtxt;🔒use rustc_macros::extension;🔒use rustc_middle::traits::solve::Certainty;🔒use rustc_middle::traits::solve::Goal;🔒use rustc_middle::traits::solve::GoalSource;🔒use rustc_middle::traits::solve::NoSolution;🔒use rustc_middle::traits::solve::QueryResult;🔒use rustc_middle::ty;🔒use rustc_middle::ty::RequiredDepth;🔒use rustc_middle::ty::TyCtxt;🔒use rustc_middle::ty::VisitorResult;🔒use rustc_middle::ty::try_visit;🔒use rustc_next_trait_solver::canonical::instantiate_canonical_state;🔒use rustc_next_trait_solver::solve::MaybeCause;🔒use rustc_next_trait_solver::solve::MaybeInfo;🔒use rustc_next_trait_solver::solve::SolverDelegateEvalExt as _;🔒use rustc_next_trait_solver::solve::inspect;🔒use rustc_span::Span;🔒use rustc_span::bug;🔒use tracing::instrument;🔒use tracing::instrument;🔒use crate::solve::delegate::SolverDelegate;🔒
Structs§
Traits§
- Infer
Ctxt Proof Tree Ext - Proof
Tree Visitor - The public API to interact with proof trees.