List of all items

Structs

• evars::EVarStore
• fixpoint_encoding::ConstInfo
• fixpoint_encoding::ExprEncodingCtxt
• fixpoint_encoding::FixpointCtxt
• fixpoint_encoding::FixpointKVar
• fixpoint_encoding::KVarDecl
• fixpoint_encoding::KVarEncodingCtxt
• fixpoint_encoding::KVarGen
• fixpoint_encoding::LocalVarEnv
• fixpoint_encoding::SortEncodingCtxt
• fixpoint_encoding::TagIdx
• fixpoint_encoding::fixpoint::AdtId
• fixpoint_encoding::fixpoint::GlobalVar
• fixpoint_encoding::fixpoint::KVid
• fixpoint_encoding::fixpoint::LocalVar
• fixpoint_encoding::fixpoint::SymStr
• fixpoint_encoding::fixpoint::fixpoint_generated::FixpointTypes
• infer::DummyEnv
• infer::InferCtxt
• infer::InferCtxtAt
• infer::InferCtxtInner
• infer::InferCtxtRoot
• infer::InferCtxtRootBuilder
• infer::Sub
• infer::Tag
• projections::Normalizer
• projections::SortNormalizer
• projections::TVarSubst
• refine_tree::Cursor
• refine_tree::Marker
• refine_tree::Node
• refine_tree::NodePtr
• refine_tree::ParentsIter
• refine_tree::RcxBind
• refine_tree::RefineCtxtTrace
• refine_tree::RefineTree
• refine_tree::Scope
• refine_tree::Unpacker
• refine_tree::WeakNodePtr

Enums

• evars::EVarState
• fixpoint_encoding::KVarEncoding
• fixpoint_encoding::Key
• fixpoint_encoding::fixpoint::DataSort
• fixpoint_encoding::fixpoint::Var
• fixpoint_encoding::fixpoint::fixpoint_generated::BinOp
• fixpoint_encoding::fixpoint::fixpoint_generated::BinRel
• fixpoint_encoding::fixpoint::fixpoint_generated::ThyFunc
• infer::ConstrReason
• infer::InferErr
• infer::SubtypeReason
• infer::TypeTrace
• projections::Candidate
• refine_tree::AssumeInvariants
• refine_tree::NodeKind

Traits

• infer::GlobalEnvExt
• infer::LocEnv
• projections::NormalizeExt

Functions

• fixpoint_encoding::bv_size_to_fixpoint
• fixpoint_encoding::const_to_fixpoint
• fixpoint_encoding::mk_implies
• infer::mk_coroutine_obligations
• projections::assemble_candidates_from_predicates
• projections::normalize_projection_ty_with_rustc
• refine_tree::children_to_fixpoint
• refine_tree::pretty::bindings_chain
• refine_tree::pretty::fmt_children
• refine_tree::pretty::preds_chain
• refine_tree::pretty::with_padding

Type Aliases

• fixpoint_encoding::ConstMap
• fixpoint_encoding::DefMap
• fixpoint_encoding::FixQueryCache
• fixpoint_encoding::fixpoint::fixpoint_generated::Bind
• fixpoint_encoding::fixpoint::fixpoint_generated::ConstDecl
• fixpoint_encoding::fixpoint::fixpoint_generated::Constant
• fixpoint_encoding::fixpoint::fixpoint_generated::Constraint
• fixpoint_encoding::fixpoint::fixpoint_generated::DataCtor
• fixpoint_encoding::fixpoint::fixpoint_generated::DataDecl
• fixpoint_encoding::fixpoint::fixpoint_generated::DataField
• fixpoint_encoding::fixpoint::fixpoint_generated::Expr
• fixpoint_encoding::fixpoint::fixpoint_generated::FunDecl
• fixpoint_encoding::fixpoint::fixpoint_generated::KVarDecl
• fixpoint_encoding::fixpoint::fixpoint_generated::Pred
• fixpoint_encoding::fixpoint::fixpoint_generated::Qualifier
• fixpoint_encoding::fixpoint::fixpoint_generated::Sort
• fixpoint_encoding::fixpoint::fixpoint_generated::SortCtor
• fixpoint_encoding::fixpoint::fixpoint_generated::Task
• infer::InferResult