List of all items

Structs

• ConfigNode
• FlatSubstitution
• FocusStack
• LabelSet
• NonEmptyVec
• PathBuf
• RawFnPtr
• RewriteRule
• RewriteRuleSet
• SimpleDag
• SlidingSum
• SmallMap
• SparseVec
• StackCalc
• StatSummary
• Stopwatch
• StringPool
• TokenBucket
• TransformStat
• TransitiveClosure
• VersionedRecord
• WindowIterator
• WriteOnce
• abstract::types::ConfigNode
• abstract::types::Fixture
• abstract::types::FlatSubstitution
• abstract::types::FocusStack
• abstract::types::LabelSet
• abstract::types::MinHeap
• abstract::types::NonEmptyVec
• abstract::types::PathBuf
• abstract::types::PrefixCounter
• abstract::types::RawFnPtr
• abstract::types::RewriteRule
• abstract::types::RewriteRuleSet
• abstract::types::SimpleDag
• abstract::types::SlidingSum
• abstract::types::SmallMap
• abstract::types::SparseVec
• abstract::types::StackCalc
• abstract::types::StatSummary
• abstract::types::Stopwatch
• abstract::types::StringPool
• abstract::types::TokenBucket
• abstract::types::TransformStat
• abstract::types::TransitiveClosure
• abstract::types::VersionedRecord
• abstract::types::WindowIterator
• abstract::types::WriteOnce
• abstract_interp::types::AbstractAlarm
• abstract_interp::types::AbstractInterpreter
• abstract_interp::types::AbstractState
• abstract_interp::types::AbstractTrace
• abstract_interp::types::AlarmCollector
• abstract_interp::types::AnalysisConfig
• abstract_interp::types::AnalysisResults
• abstract_interp::types::CallGraph
• abstract_interp::types::CallGraphNode
• abstract_interp::types::ChaoticIterator
• abstract_interp::types::CongruenceDomain
• abstract_interp::types::CostBound
• abstract_interp::types::DepthDomain
• abstract_interp::types::FixpointEngine
• abstract_interp::types::FunctionSummary
• abstract_interp::types::InterpretationSummary
• abstract_interp::types::Interval
• abstract_interp::types::IntervalEnv
• abstract_interp::types::IntervalParityProduct
• abstract_interp::types::PowersetDomain
• abstract_interp::types::ProductDomain
• abstract_interp::types::ReachabilityAnalysis
• abstract_interp::types::SimpleAbstractInterpreter
• abstract_interp::types::SummaryDatabase
• abstract_interp::types::TransferFunction
• alpha::types::AlphaCache
• alpha::types::ConfigNode
• alpha::types::Fixture
• alpha::types::FlatSubstitution
• alpha::types::FocusStack
• alpha::types::LabelSet
• alpha::types::MinHeap
• alpha::types::NonEmptyVec
• alpha::types::PathBuf
• alpha::types::PrefixCounter
• alpha::types::RawFnPtr
• alpha::types::RewriteRule
• alpha::types::RewriteRuleSet
• alpha::types::SimpleDag
• alpha::types::SlidingSum
• alpha::types::SmallMap
• alpha::types::SparseVec
• alpha::types::StackCalc
• alpha::types::StatSummary
• alpha::types::Stopwatch
• alpha::types::StringPool
• alpha::types::TokenBucket
• alpha::types::TransformStat
• alpha::types::TransitiveClosure
• alpha::types::VersionedRecord
• alpha::types::WindowIterator
• alpha::types::WriteOnce
• arena::types::AnnotationTable
• arena::types::Arena
• arena::types::ArenaBlock
• arena::types::ArenaCheckpoint
• arena::types::ArenaMap
• arena::types::ArenaPool
• arena::types::ArenaStats
• arena::types::ArenaStatsExt
• arena::types::ArenaString
• arena::types::ArenaVec
• arena::types::BiMap
• arena::types::BumpArena
• arena::types::ChainedArena
• arena::types::DiagMeta
• arena::types::DoubleArena
• arena::types::EventCounter
• arena::types::FrequencyTable
• arena::types::GrowableArena
• arena::types::IdDispenser
• arena::types::Idx
• arena::types::IdxRange
• arena::types::InterningArena
• arena::types::IntervalSet
• arena::types::LinearArena
• arena::types::LoopClock
• arena::types::MemoSlot
• arena::types::MemoryRegion
• arena::types::MemoryRegionRegistry
• arena::types::PoolArena
• arena::types::ScopeStack
• arena::types::ScopedArena
• arena::types::ScopedArenaExt
• arena::types::SimpleLruCache
• arena::types::SlabArena
• arena::types::Slot
• arena::types::SparseBitSet
• arena::types::StatCache
• arena::types::StringInterner
• arena::types::Timestamp
• arena::types::TwoGenerationArena
• arena::types::TypedArena
• arena::types::TypedId
• arena::types::WorkQueue
• arena::types::WorkStack
• axiom::types::AxiomAllowlist
• axiom::types::AxiomSafetyReport
• axiom::types::AxiomSequence
• axiom::types::AxiomUsageRecord
• axiom::types::AxiomValidator
• axiom::types::BitSet64
• axiom::types::BucketCounter
• axiom::types::ConfigNode
• axiom::types::Fixture
• axiom::types::FlatSubstitution
• axiom::types::FocusStack
• axiom::types::LabelSet
• axiom::types::MinHeap
• axiom::types::NonEmptyVec
• axiom::types::PathBuf
• axiom::types::PrefixCounter
• axiom::types::RawFnPtr
• axiom::types::RewriteRule
• axiom::types::RewriteRuleSet
• axiom::types::SimpleDag
• axiom::types::SlidingSum
• axiom::types::SmallMap
• axiom::types::SparseVec
• axiom::types::StackCalc
• axiom::types::StatSummary
• axiom::types::Stopwatch
• axiom::types::StringPool
• axiom::types::TokenBucket
• axiom::types::TransformStat
• axiom::types::TransitiveClosure
• axiom::types::VersionedRecord
• axiom::types::WindowIterator
• axiom::types::WriteOnce
• bench_support::types::AdaptiveWarmup
• bench_support::types::BatchTimer
• bench_support::types::BenchAnnotation
• bench_support::types::BenchAnnotationSet
• bench_support::types::BenchConfig
• bench_support::types::BenchEventLog
• bench_support::types::BenchFilter
• bench_support::types::BenchGroup
• bench_support::types::BenchHarnessExt
• bench_support::types::BenchHarnessV2
• bench_support::types::BenchHistogram
• bench_support::types::BenchMatrix
• bench_support::types::BenchPlan
• bench_support::types::BenchProfiler
• bench_support::types::BenchRegistry
• bench_support::types::BenchReporter
• bench_support::types::BenchResult
• bench_support::types::BenchResultExt
• bench_support::types::BenchSuite
• bench_support::types::BenchSummary
• bench_support::types::BenchTimer
• bench_support::types::ColdCacheSimulator
• bench_support::types::ConfidenceInterval
• bench_support::types::CpuPinner
• bench_support::types::FuzzInput
• bench_support::types::HdrHistogram
• bench_support::types::HistogramBin
• bench_support::types::LatencyPercentile
• bench_support::types::Metric
• bench_support::types::MetricSet
• bench_support::types::MovingAverage
• bench_support::types::MultiArmBandit
• bench_support::types::OlsRegression
• bench_support::types::ProgressBar
• bench_support::types::RegressionTest
• bench_support::types::SampleBuffer
• bench_support::types::ScalingTest
• bench_support::types::StabilityChecker
• bench_support::types::ThroughputTracker
• bench_support::types::TimeSlice
• beta::types::BetaStats
• beta::types::ConfigNode
• beta::types::FlatSubstitution
• beta::types::FocusStack
• beta::types::LabelSet
• beta::types::NonEmptyVec
• beta::types::PathBuf
• beta::types::RawFnPtr
• beta::types::RewriteRule
• beta::types::RewriteRuleSet
• beta::types::SimpleDag
• beta::types::SlidingSum
• beta::types::SmallMap
• beta::types::SparseVec
• beta::types::StackCalc
• beta::types::StatSummary
• beta::types::Stopwatch
• beta::types::StringPool
• beta::types::TokenBucket
• beta::types::TransformStat
• beta::types::TransitiveClosure
• beta::types::VersionedRecord
• beta::types::WindowIterator
• beta::types::WriteOnce
• builtin::types::BuiltinInfo
• builtin::types::ConfigNode
• builtin::types::FlatSubstitution
• builtin::types::FocusStack
• builtin::types::LabelSet
• builtin::types::NonEmptyVec
• builtin::types::PathBuf
• builtin::types::RawFnPtr
• builtin::types::RewriteRule
• builtin::types::RewriteRuleSet
• builtin::types::SimpleDag
• builtin::types::SlidingSum
• builtin::types::SmallMap
• builtin::types::SparseVec
• builtin::types::StackCalc
• builtin::types::StatSummary
• builtin::types::Stopwatch
• builtin::types::StringPool
• builtin::types::TokenBucket
• builtin::types::TransformStat
• builtin::types::TransitiveClosure
• builtin::types::VersionedRecord
• builtin::types::WindowIterator
• builtin::types::WriteOnce
• cache::types::BloomFilterApprox
• cache::types::CacheManager
• cache::types::CacheStatistics
• cache::types::ConfigNode
• cache::types::DefEqCache
• cache::types::FlatSubstitution
• cache::types::FocusStack
• cache::types::InferCache
• cache::types::LabelSet
• cache::types::LruCache
• cache::types::MultiLevelCache
• cache::types::NonEmptyVec
• cache::types::PathBuf
• cache::types::RawFnPtr
• cache::types::RewriteRule
• cache::types::RewriteRuleSet
• cache::types::SimpleDag
• cache::types::SlidingSum
• cache::types::SmallMap
• cache::types::SparseVec
• cache::types::StackCalc
• cache::types::StatSummary
• cache::types::Stopwatch
• cache::types::StringPool
• cache::types::TokenBucket
• cache::types::TransformStat
• cache::types::TransitiveClosure
• cache::types::TtlCache
• cache::types::VersionedRecord
• cache::types::WhnfCache
• cache::types::WindowIterator
• cache::types::WriteOnce
• check::types::BatchCheckResult
• check::types::CheckConfig
• check::types::CheckStats
• check::types::ConfigNode
• check::types::DeclSummary
• check::types::EnvBuilder
• check::types::FlatSubstitution
• check::types::FocusStack
• check::types::LabelSet
• check::types::NonEmptyVec
• check::types::PathBuf
• check::types::RawFnPtr
• check::types::RewriteRule
• check::types::RewriteRuleSet
• check::types::SimpleDag
• check::types::SlidingSum
• check::types::SmallMap
• check::types::SparseVec
• check::types::StackCalc
• check::types::StatSummary
• check::types::Stopwatch
• check::types::StringPool
• check::types::TempEnvScope
• check::types::TokenBucket
• check::types::TransformStat
• check::types::TransitiveClosure
• check::types::VersionedRecord
• check::types::WindowIterator
• check::types::WriteOnce
• congruence::types::ConfigNode
• congruence::types::CongrClosureStats
• congruence::types::CongrHypothesis
• congruence::types::CongrLemmaCache
• congruence::types::CongruenceClosure
• congruence::types::CongruenceTheorem
• congruence::types::EGraph
• congruence::types::ENode
• congruence::types::Fixture
• congruence::types::FlatApp
• congruence::types::FlatCC
• congruence::types::FlatSubstitution
• congruence::types::FocusStack
• congruence::types::InstrumentedCC
• congruence::types::LabelSet
• congruence::types::MinHeap
• congruence::types::NonEmptyVec
• congruence::types::PathBuf
• congruence::types::PrefixCounter
• congruence::types::RawFnPtr
• congruence::types::RewriteRule
• congruence::types::RewriteRuleSet
• congruence::types::SimpleDag
• congruence::types::SlidingSum
• congruence::types::SmallMap
• congruence::types::SparseVec
• congruence::types::StackCalc
• congruence::types::StatSummary
• congruence::types::Stopwatch
• congruence::types::StringPool
• congruence::types::TokenBucket
• congruence::types::TransformStat
• congruence::types::TransitiveClosure
• congruence::types::VersionedRecord
• congruence::types::WindowIterator
• congruence::types::WriteOnce
• context::types::ConfigNode
• context::types::Context
• context::types::ContextChain
• context::types::ContextDiff
• context::types::ContextEntry
• context::types::ContextSnapshot
• context::types::ContextStats
• context::types::FlatSubstitution
• context::types::FocusStack
• context::types::FreshNameSeq
• context::types::HypContext
• context::types::LabelSet
• context::types::LocalVar
• context::types::NameGenerator
• context::types::NonEmptyVec
• context::types::PathBuf
• context::types::RawFnPtr
• context::types::RewriteRule
• context::types::RewriteRuleSet
• context::types::ScopedContext
• context::types::SimpleDag
• context::types::SlidingSum
• context::types::SmallMap
• context::types::SparseVec
• context::types::StackCalc
• context::types::StatSummary
• context::types::Stopwatch
• context::types::StringPool
• context::types::TokenBucket
• context::types::TransformStat
• context::types::TransitiveClosure
• context::types::VersionedRecord
• context::types::WindowIterator
• context::types::WriteOnce
• conversion::types::BitSet64
• conversion::types::BucketCounter
• conversion::types::Coercion
• conversion::types::CoercionTable
• conversion::types::ConfigNode
• conversion::types::ConversionChecker
• conversion::types::Fixture
• conversion::types::FlatSubstitution
• conversion::types::FocusStack
• conversion::types::LabelSet
• conversion::types::MinHeap
• conversion::types::NonEmptyVec
• conversion::types::PathBuf
• conversion::types::PrefixCounter
• conversion::types::RawFnPtr
• conversion::types::RewriteRule
• conversion::types::RewriteRuleSet
• conversion::types::SimpleDag
• conversion::types::SlidingSum
• conversion::types::SmallMap
• conversion::types::SparseVec
• conversion::types::StackCalc
• conversion::types::StatSummary
• conversion::types::Stopwatch
• conversion::types::StringPool
• conversion::types::TokenBucket
• conversion::types::TransformStat
• conversion::types::TransitiveClosure
• conversion::types::VersionedRecord
• conversion::types::WindowIterator
• conversion::types::WriteOnce
• declaration::types::AnnotationTable
• declaration::types::AxiomVal
• declaration::types::BeforeAfter
• declaration::types::BiMap
• declaration::types::ConstantSummary
• declaration::types::ConstantVal
• declaration::types::ConstructorVal
• declaration::types::DeclDependencies
• declaration::types::DeclFilter
• declaration::types::DeclIndex
• declaration::types::DeclSignature
• declaration::types::DefinitionVal
• declaration::types::DiagMeta
• declaration::types::EventCounter
• declaration::types::FrequencyTable
• declaration::types::Generation
• declaration::types::IdDispenser
• declaration::types::InductiveVal
• declaration::types::IntervalSet
• declaration::types::LoopClock
• declaration::types::MemoSlot
• declaration::types::OpaqueVal
• declaration::types::QuotVal
• declaration::types::RecursorRule
• declaration::types::RecursorVal
• declaration::types::RingBuffer
• declaration::types::ScopeStack
• declaration::types::SeqNum
• declaration::types::SimpleLruCache
• declaration::types::Slot
• declaration::types::SparseBitSet
• declaration::types::StatCache
• declaration::types::StringInterner
• declaration::types::TheoremVal
• declaration::types::Timestamp
• declaration::types::TypedId
• declaration::types::WorkQueue
• declaration::types::WorkStack
• def_eq::types::BatchDefEqChecker
• def_eq::types::ConfigNode
• def_eq::types::DefEqChecker
• def_eq::types::DefEqConfig
• def_eq::types::DefEqStats
• def_eq::types::FlatSubstitution
• def_eq::types::FocusStack
• def_eq::types::LabelSet
• def_eq::types::NameIndex
• def_eq::types::NonEmptyVec
• def_eq::types::PathBuf
• def_eq::types::RawFnPtr
• def_eq::types::RewriteRule
• def_eq::types::RewriteRuleSet
• def_eq::types::SimpleDag
• def_eq::types::SlidingSum
• def_eq::types::SmallMap
• def_eq::types::SparseVec
• def_eq::types::StackCalc
• def_eq::types::StatSummary
• def_eq::types::Stopwatch
• def_eq::types::StringPool
• def_eq::types::StringTrie
• def_eq::types::TokenBucket
• def_eq::types::TransformStat
• def_eq::types::TransitiveClosure
• def_eq::types::VersionedRecord
• def_eq::types::WindowIterator
• def_eq::types::WriteOnce
• env::types::ConfigNode
• env::types::EnvKindCounts
• env::types::EnvStats
• env::types::Environment
• env::types::EnvironmentBuilder
• env::types::EnvironmentSnapshot
• env::types::EnvironmentView
• env::types::Fixture
• env::types::FlatSubstitution
• env::types::FocusStack
• env::types::LabelSet
• env::types::MinHeap
• env::types::NonEmptyVec
• env::types::PathBuf
• env::types::PrefixCounter
• env::types::RawFnPtr
• env::types::RewriteRule
• env::types::RewriteRuleSet
• env::types::SimpleDag
• env::types::SlidingSum
• env::types::SmallMap
• env::types::SparseVec
• env::types::StackCalc
• env::types::StatSummary
• env::types::Stopwatch
• env::types::StringPool
• env::types::TokenBucket
• env::types::TransformStat
• env::types::TransitiveClosure
• env::types::VersionedRecord
• env::types::WindowIterator
• env::types::WriteOnce
• equiv_manager::types::AnnotationTable
• equiv_manager::types::BeforeAfter
• equiv_manager::types::BiMap
• equiv_manager::types::CheckedEquiv
• equiv_manager::types::DiagMeta
• equiv_manager::types::EquivClass
• equiv_manager::types::EquivManager
• equiv_manager::types::EquivManagerStats
• equiv_manager::types::EquivQuery
• equiv_manager::types::EquivStats
• equiv_manager::types::EquivalenceTable
• equiv_manager::types::EventCounter
• equiv_manager::types::ExprEquivCache
• equiv_manager::types::FrequencyTable
• equiv_manager::types::Generation
• equiv_manager::types::IdDispenser
• equiv_manager::types::IndexEquivManager
• equiv_manager::types::InstrumentedEquivManager
• equiv_manager::types::IntervalSet
• equiv_manager::types::LoopClock
• equiv_manager::types::MemoSlot
• equiv_manager::types::PersistentEquivManager
• equiv_manager::types::RingBuffer
• equiv_manager::types::ScopeStack
• equiv_manager::types::ScopedEquivManager
• equiv_manager::types::SeqNum
• equiv_manager::types::SimpleLruCache
• equiv_manager::types::Slot
• equiv_manager::types::SparseBitSet
• equiv_manager::types::StatCache
• equiv_manager::types::StringInterner
• equiv_manager::types::SymmetricRelation
• equiv_manager::types::Timestamp
• equiv_manager::types::TypedId
• equiv_manager::types::UnionFind
• equiv_manager::types::WorkQueue
• equiv_manager::types::WorkStack
• error::types::AnnotatedError
• error::types::ConfigNode
• error::types::Diagnostic
• error::types::DiagnosticCollection
• error::types::ErrorAccumulator
• error::types::ErrorContext
• error::types::ErrorNote
• error::types::ErrorReport
• error::types::Fixture
• error::types::FlatSubstitution
• error::types::FocusStack
• error::types::LabelSet
• error::types::MinHeap
• error::types::NonEmptyVec
• error::types::PathBuf
• error::types::PhasedError
• error::types::PrefixCounter
• error::types::RawFnPtr
• error::types::RewriteRule
• error::types::RewriteRuleSet
• error::types::SimpleDag
• error::types::SlidingSum
• error::types::SmallMap
• error::types::SparseVec
• error::types::StackCalc
• error::types::StatSummary
• error::types::Stopwatch
• error::types::StringPool
• error::types::TokenBucket
• error::types::TransformStat
• error::types::TransitiveClosure
• error::types::VersionedRecord
• error::types::WindowIterator
• error::types::WriteOnce
• eta::types::ConfigNode
• eta::types::EtaChecker
• eta::types::EtaJob
• eta::types::EtaJobQueue
• eta::types::EtaLog
• eta::types::EtaNormInfo
• eta::types::EtaNormalCache
• eta::types::EtaOpCounter
• eta::types::EtaReductionStats
• eta::types::EtaRewriteRule
• eta::types::EtaStatCounter
• eta::types::FocusStack
• eta::types::LabelSet
• eta::types::LambdaStats
• eta::types::NonEmptyVec
• eta::types::PathBuf
• eta::types::RawFnPtr
• eta::types::RewriteRule
• eta::types::SimpleDag
• eta::types::SlidingSum
• eta::types::SmallMap
• eta::types::StatSummary
• eta::types::StringPool
• eta::types::TokenBucket
• eta::types::TransformStat
• eta::types::TransitiveClosure
• eta::types::VersionedRecord
• eta::types::WindowIterator
• export::types::ConfigNode
• export::types::ExportedModule
• export::types::FocusStack
• export::types::LabelSet
• export::types::ModuleCache
• export::types::ModuleDependencyGraph
• export::types::ModuleDiff
• export::types::ModuleInfo
• export::types::ModuleRegistry
• export::types::ModuleVersion
• export::types::NonEmptyVec
• export::types::PathBuf
• export::types::RawFnPtr
• export::types::RewriteRule
• export::types::RewriteRuleSet
• export::types::SimpleDag
• export::types::SlidingSum
• export::types::SmallMap
• export::types::StatSummary
• export::types::StringPool
• export::types::TokenBucket
• export::types::TransformStat
• export::types::TransitiveClosure
• export::types::VersionedRecord
• export::types::WindowIterator
• expr::types::ConfigNode
• expr::types::FVarId
• expr::types::FVarIdGen
• expr::types::Fixture
• expr::types::FlatSubstitution
• expr::types::FocusStack
• expr::types::LabelSet
• expr::types::MinHeap
• expr::types::NonEmptyVec
• expr::types::PathBuf
• expr::types::PrefixCounter
• expr::types::RawFnPtr
• expr::types::RewriteRule
• expr::types::RewriteRuleSet
• expr::types::SimpleDag
• expr::types::SlidingSum
• expr::types::SmallMap
• expr::types::SparseVec
• expr::types::StackCalc
• expr::types::StatSummary
• expr::types::Stopwatch
• expr::types::StringPool
• expr::types::TokenBucket
• expr::types::TransformStat
• expr::types::TransitiveClosure
• expr::types::VersionedRecord
• expr::types::WindowIterator
• expr::types::WriteOnce
• expr_cache::types::BitSet64
• expr_cache::types::BucketCounter
• expr_cache::types::CacheSessionStats
• expr_cache::types::ConfigNode
• expr_cache::types::EvictionTracker
• expr_cache::types::ExprHashcons
• expr_cache::types::ExprId
• expr_cache::types::ExprPool
• expr_cache::types::Fixture
• expr_cache::types::FlatSubstitution
• expr_cache::types::FocusStack
• expr_cache::types::InvalidationSet
• expr_cache::types::LabelSet
• expr_cache::types::MemoTable
• expr_cache::types::MinHeap
• expr_cache::types::NonEmptyVec
• expr_cache::types::PathBuf
• expr_cache::types::PathCache
• expr_cache::types::PrefixCounter
• expr_cache::types::RawFnPtr
• expr_cache::types::RcExprPool
• expr_cache::types::RewriteRule
• expr_cache::types::RewriteRuleSet
• expr_cache::types::SharedCacheEntry
• expr_cache::types::SimpleDag
• expr_cache::types::SlidingSum
• expr_cache::types::SmallMap
• expr_cache::types::SparseVec
• expr_cache::types::StackCalc
• expr_cache::types::StatSummary
• expr_cache::types::Stopwatch
• expr_cache::types::StringPool
• expr_cache::types::TokenBucket
• expr_cache::types::TransformStat
• expr_cache::types::TransitiveClosure
• expr_cache::types::TwoLevelCache
• expr_cache::types::VersionedCache
• expr_cache::types::VersionedRecord
• expr_cache::types::WindowIterator
• expr_cache::types::WriteOnce
• expr_util::types::ConfigNode
• expr_util::types::Fixture
• expr_util::types::FlatSubstitution
• expr_util::types::FocusStack
• expr_util::types::LabelSet
• expr_util::types::MinHeap
• expr_util::types::NonEmptyVec
• expr_util::types::PathBuf
• expr_util::types::PrefixCounter
• expr_util::types::RawFnPtr
• expr_util::types::RewriteRule
• expr_util::types::RewriteRuleSet
• expr_util::types::SimpleDag
• expr_util::types::SlidingSum
• expr_util::types::SmallMap
• expr_util::types::SparseVec
• expr_util::types::StackCalc
• expr_util::types::StatSummary
• expr_util::types::Stopwatch
• expr_util::types::StringPool
• expr_util::types::TokenBucket
• expr_util::types::TransformStat
• expr_util::types::TransitiveClosure
• expr_util::types::VersionedRecord
• expr_util::types::WindowIterator
• expr_util::types::WriteOnce
• ffi::types::BuiltinExterns
• ffi::types::ConfigNode
• ffi::types::ExternDecl
• ffi::types::ExternRegistry
• ffi::types::FfiSignature
• ffi::types::Fixture
• ffi::types::FlatSubstitution
• ffi::types::FocusStack
• ffi::types::LabelSet
• ffi::types::LibraryManifest
• ffi::types::LibraryVersion
• ffi::types::MinHeap
• ffi::types::NonEmptyVec
• ffi::types::PathBuf
• ffi::types::PrefixCounter
• ffi::types::RawFnPtr
• ffi::types::RewriteRule
• ffi::types::RewriteRuleSet
• ffi::types::SimpleDag
• ffi::types::SlidingSum
• ffi::types::SmallMap
• ffi::types::SparseVec
• ffi::types::StackCalc
• ffi::types::StatSummary
• ffi::types::Stopwatch
• ffi::types::StringPool
• ffi::types::SymbolMetadata
• ffi::types::TokenBucket
• ffi::types::TransformStat
• ffi::types::TransitiveClosure
• ffi::types::VersionedRecord
• ffi::types::WindowIterator
• ffi::types::WriteOnce
• inductive::types::ConfigNode
• inductive::types::FocusStack
• inductive::types::InductiveEnv
• inductive::types::InductiveFamily
• inductive::types::InductiveType
• inductive::types::InductiveTypeBuilder
• inductive::types::InductiveTypeInfo
• inductive::types::IntroRule
• inductive::types::LabelSet
• inductive::types::NonEmptyVec
• inductive::types::RecursorBuilder
• inductive::types::SimpleDag
• inductive::types::SmallMap
• inductive::types::StatSummary
• inductive::types::TransformStat
• inductive::types::VersionedRecord
• inductive::types::WindowIterator
• infer::types::ConfigNode
• infer::types::FlatSubstitution
• infer::types::FocusStack
• infer::types::InferCache
• infer::types::InferCacheEntry
• infer::types::InferStats
• infer::types::LabelSet
• infer::types::LocalDecl
• infer::types::NonEmptyVec
• infer::types::PathBuf
• infer::types::RawFnPtr
• infer::types::RewriteRule
• infer::types::RewriteRuleSet
• infer::types::SimpleDag
• infer::types::SlidingSum
• infer::types::SmallMap
• infer::types::SparseVec
• infer::types::StackCalc
• infer::types::StatSummary
• infer::types::Stopwatch
• infer::types::StringPool
• infer::types::TokenBucket
• infer::types::TransformStat
• infer::types::TransitiveClosure
• infer::types::TypeChecker
• infer::types::TypingJudgment
• infer::types::VersionedRecord
• infer::types::WindowIterator
• infer::types::WriteOnce
• instantiate::types::ConfigNode
• instantiate::types::Fixture
• instantiate::types::FlatSubstitution
• instantiate::types::FocusStack
• instantiate::types::LabelSet
• instantiate::types::MinHeap
• instantiate::types::NamedSubst
• instantiate::types::NonEmptyVec
• instantiate::types::PathBuf
• instantiate::types::PrefixCounter
• instantiate::types::RawFnPtr
• instantiate::types::RewriteRule
• instantiate::types::RewriteRuleSet
• instantiate::types::SimpleDag
• instantiate::types::SlidingSum
• instantiate::types::SmallMap
• instantiate::types::SparseVec
• instantiate::types::StackCalc
• instantiate::types::StatSummary
• instantiate::types::Stopwatch
• instantiate::types::StringPool
• instantiate::types::Telescope
• instantiate::types::TokenBucket
• instantiate::types::TransformStat
• instantiate::types::TransitiveClosure
• instantiate::types::VersionedRecord
• instantiate::types::WindowIterator
• instantiate::types::WriteOnce
• level::types::ConfigNode
• level::types::ConstraintSet
• level::types::Fixture
• level::types::FlatSubstitution
• level::types::FocusStack
• level::types::LabelSet
• level::types::LevelMVarId
• level::types::MinHeap
• level::types::NonEmptyVec
• level::types::PathBuf
• level::types::PrefixCounter
• level::types::RawFnPtr
• level::types::RewriteRule
• level::types::RewriteRuleSet
• level::types::SimpleDag
• level::types::SlidingSum
• level::types::SmallMap
• level::types::SparseVec
• level::types::StackCalc
• level::types::StatSummary
• level::types::Stopwatch
• level::types::StringPool
• level::types::TokenBucket
• level::types::TransformStat
• level::types::TransitiveClosure
• level::types::VersionedRecord
• level::types::WindowIterator
• level::types::WriteOnce
• match_compile::types::CompileResult
• match_compile::types::ConfigNode
• match_compile::types::ConstructorInfo
• match_compile::types::FlatSubstitution
• match_compile::types::FocusStack
• match_compile::types::LabelSet
• match_compile::types::MatchArm
• match_compile::types::MatchCompiler
• match_compile::types::MatchStats
• match_compile::types::NonEmptyVec
• match_compile::types::PathBuf
• match_compile::types::PatternStats
• match_compile::types::RawFnPtr
• match_compile::types::RewriteRule
• match_compile::types::RewriteRuleSet
• match_compile::types::SimpleDag
• match_compile::types::SlidingSum
• match_compile::types::SmallMap
• match_compile::types::SparseVec
• match_compile::types::StackCalc
• match_compile::types::StatSummary
• match_compile::types::Stopwatch
• match_compile::types::StringPool
• match_compile::types::TokenBucket
• match_compile::types::TransformStat
• match_compile::types::TransitiveClosure
• match_compile::types::VersionedRecord
• match_compile::types::WindowIterator
• match_compile::types::WriteOnce
• name::types::AnnotationTable
• name::types::BeforeAfter
• name::types::BiMap
• name::types::DiagMeta
• name::types::EventCounter
• name::types::FrequencyTable
• name::types::Generation
• name::types::IdDispenser
• name::types::IntervalSet
• name::types::LoopClock
• name::types::MemoSlot
• name::types::NameGenerator
• name::types::NameGeneratorExt
• name::types::NameMap
• name::types::NameMapping
• name::types::NamePool
• name::types::NameResolver
• name::types::NameSet
• name::types::NameSetExt
• name::types::NameTrie
• name::types::NameTrieExt
• name::types::QualifiedName
• name::types::QualifiedNameExt
• name::types::RingBuffer
• name::types::ScopeStack
• name::types::SeqNum
• name::types::SimpleLruCache
• name::types::Slot
• name::types::SparseBitSet
• name::types::StatCache
• name::types::StringInterner
• name::types::Timestamp
• name::types::TypedId
• name::types::WorkQueue
• name::types::WorkStack
• no_std_compat::types::AddrRange
• no_std_compat::types::AllocConfig
• no_std_compat::types::AllocStats
• no_std_compat::types::AtomicVersion
• no_std_compat::types::Budget
• no_std_compat::types::BuildInfo
• no_std_compat::types::BumpAlloc
• no_std_compat::types::CapabilitySet
• no_std_compat::types::CfgSnapshot
• no_std_compat::types::CodeSection
• no_std_compat::types::CompatLayer
• no_std_compat::types::CompatMatrix
• no_std_compat::types::CompatibilityReport
• no_std_compat::types::CompileFlags
• no_std_compat::types::ConditionalInit
• no_std_compat::types::CounterCell
• no_std_compat::types::CrossPlatformTimer
• no_std_compat::types::EnvFlags
• no_std_compat::types::FeatureFlags
• no_std_compat::types::InstructionBuffer
• no_std_compat::types::LibraryManifest
• no_std_compat::types::LinearScanAllocator
• no_std_compat::types::MemoryLayout
• no_std_compat::types::NoStdHashMap
• no_std_compat::types::NoStdRingBuf
• no_std_compat::types::ObjectFile
• no_std_compat::types::PageMap
• no_std_compat::types::PanicSink
• no_std_compat::types::PlatformCaps
• no_std_compat::types::PlatformInfo
• no_std_compat::types::RelocEntry
• no_std_compat::types::RuntimeVersion
• no_std_compat::types::ScratchBuffer
• no_std_compat::types::SharedMemHandle
• no_std_compat::types::ShimRegistry
• no_std_compat::types::SpinFlag
• no_std_compat::types::StackGuard
• no_std_compat::types::StdCompat
• no_std_compat::types::SymbolTable
• no_std_compat::types::TargetTriple
• no_std_compat::types::VersionConstraint
• no_std_compat::types::WasmFeatureSet
• no_std_compat::types::WasmMemRegion
• no_std_compat::types::WasmMemTable
• normalize::types::ConfigNode
• normalize::types::Fixture
• normalize::types::FlatSubstitution
• normalize::types::FocusStack
• normalize::types::LabelSet
• normalize::types::LazyNormal
• normalize::types::MemoizedNormalizer
• normalize::types::MinHeap
• normalize::types::NonEmptyVec
• normalize::types::NormStats
• normalize::types::PathBuf
• normalize::types::PrefixCounter
• normalize::types::RawFnPtr
• normalize::types::RewriteRule
• normalize::types::RewriteRuleSet
• normalize::types::SimpleDag
• normalize::types::SlidingSum
• normalize::types::SmallMap
• normalize::types::SparseVec
• normalize::types::StackCalc
• normalize::types::StatSummary
• normalize::types::Stopwatch
• normalize::types::StringPool
• normalize::types::TokenBucket
• normalize::types::TransformStat
• normalize::types::TransitiveClosure
• normalize::types::VersionedRecord
• normalize::types::WindowIterator
• normalize::types::WriteOnce
• prettyprint::types::AnnotationTable
• prettyprint::types::BiMap
• prettyprint::types::BoxedPrinter
• prettyprint::types::ColorScheme
• prettyprint::types::DiagMeta
• prettyprint::types::DocBuilder
• prettyprint::types::EscapeHelper
• prettyprint::types::EventCounter
• prettyprint::types::ExprPrinter
• prettyprint::types::FmtWidth
• prettyprint::types::FrequencyTable
• prettyprint::types::IdDispenser
• prettyprint::types::IntervalSet
• prettyprint::types::LoopClock
• prettyprint::types::MemoSlot
• prettyprint::types::PrettyConfig
• prettyprint::types::PrettyPrinterState
• prettyprint::types::PrettyTable
• prettyprint::types::PrintConfig
• prettyprint::types::SExprPrinter
• prettyprint::types::ScopeStack
• prettyprint::types::SimpleLruCache
• prettyprint::types::Slot
• prettyprint::types::SparseBitSet
• prettyprint::types::StatCache
• prettyprint::types::StringInterner
• prettyprint::types::Timestamp
• prettyprint::types::TokenPrinter
• prettyprint::types::TypedId
• prettyprint::types::WorkQueue
• prettyprint::types::WorkStack
• proof::types::ConfigNode
• proof::types::Fixture
• proof::types::FlatSubstitution
• proof::types::FocusStack
• proof::types::LabelSet
• proof::types::MinHeap
• proof::types::NonEmptyVec
• proof::types::PathBuf
• proof::types::PrefixCounter
• proof::types::ProofAnalysis
• proof::types::ProofAnalyzer
• proof::types::ProofCertificate
• proof::types::ProofNormalizer
• proof::types::ProofObligation
• proof::types::ProofSkeleton
• proof::types::ProofState
• proof::types::ProofTerm
• proof::types::RawFnPtr
• proof::types::RewriteRule
• proof::types::RewriteRuleSet
• proof::types::SimpleDag
• proof::types::SlidingSum
• proof::types::SmallMap
• proof::types::SparseVec
• proof::types::StackCalc
• proof::types::StatSummary
• proof::types::Stopwatch
• proof::types::StringPool
• proof::types::TokenBucket
• proof::types::TransformStat
• proof::types::TransitiveClosure
• proof::types::VersionedRecord
• proof::types::WindowIterator
• proof::types::WriteOnce
• quotient::types::ConfigNode
• quotient::types::EquivClassSystem
• quotient::types::FocusStack
• quotient::types::LabelSet
• quotient::types::NonEmptyVec
• quotient::types::PathBuf
• quotient::types::QuotLiftCache
• quotient::types::QuotReductionStep
• quotient::types::QuotStats
• quotient::types::QuotientBuilder
• quotient::types::QuotientDescription
• quotient::types::QuotientKernel
• quotient::types::QuotientNormalizer
• quotient::types::QuotientReducer
• quotient::types::QuotientType
• quotient::types::RawFnPtr
• quotient::types::RewriteRule
• quotient::types::RewriteRuleSet
• quotient::types::SimpleDag
• quotient::types::SlidingSum
• quotient::types::SmallMap
• quotient::types::StatSummary
• quotient::types::StringPool
• quotient::types::TokenBucket
• quotient::types::TransformStat
• quotient::types::TransitiveClosure
• quotient::types::VersionedRecord
• quotient::types::WindowIterator
• reduce::types::ConfigNode
• reduce::types::FlatSubstitution
• reduce::types::FocusStack
• reduce::types::LabelSet
• reduce::types::NonEmptyVec
• reduce::types::PathBuf
• reduce::types::RawFnPtr
• reduce::types::Reducer
• reduce::types::ReducerStats
• reduce::types::ReductionStep
• reduce::types::ReductionTrace
• reduce::types::RewriteRule
• reduce::types::RewriteRuleSet
• reduce::types::SimpleDag
• reduce::types::SlidingSum
• reduce::types::SmallMap
• reduce::types::SparseVec
• reduce::types::StackCalc
• reduce::types::StatSummary
• reduce::types::Stopwatch
• reduce::types::StringPool
• reduce::types::TokenBucket
• reduce::types::TransformStat
• reduce::types::TransitiveClosure
• reduce::types::VersionedRecord
• reduce::types::WindowIterator
• reduce::types::WriteOnce
• reduction::types::ConfigNode
• reduction::types::Fixture
• reduction::types::FlatSubstitution
• reduction::types::FocusStack
• reduction::types::LabelSet
• reduction::types::MinHeap
• reduction::types::NonEmptyVec
• reduction::types::PathBuf
• reduction::types::PrefixCounter
• reduction::types::RawFnPtr
• reduction::types::RedexInfo
• reduction::types::ReductionMemo
• reduction::types::ReductionStats
• reduction::types::ReductionStep
• reduction::types::ReductionTrace
• reduction::types::RewriteRule
• reduction::types::RewriteRuleSet
• reduction::types::SimpleDag
• reduction::types::SlidingSum
• reduction::types::SmallMap
• reduction::types::SparseVec
• reduction::types::StackCalc
• reduction::types::StatSummary
• reduction::types::Stopwatch
• reduction::types::StringPool
• reduction::types::TokenBucket
• reduction::types::TransformStat
• reduction::types::TransitiveClosure
• reduction::types::VersionedRecord
• reduction::types::WindowIterator
• reduction::types::WriteOnce
• serial::types::BinarySection
• serial::types::BlobValidator
• serial::types::BufferedOleanWriter
• serial::types::CheckpointedReader
• serial::types::ChecksummedWriter
• serial::types::CompatibilityChecker
• serial::types::DeclDiff
• serial::types::DeclIndex
• serial::types::DeclKindSet
• serial::types::DeltaList
• serial::types::FileStats
• serial::types::FormatDiagnostics
• serial::types::MetadataReader
• serial::types::MetadataWriter
• serial::types::NameTable
• serial::types::OleanArchive
• serial::types::OleanHeader
• serial::types::OleanReader
• serial::types::OleanWriter
• serial::types::SectionHeader
• serial::types::SectionTable
• serial::types::SerialError
• serial::types::StringPool
• simp::types::ConfigNode
• simp::types::Fixture
• simp::types::FlatSubstitution
• simp::types::FocusStack
• simp::types::LabelSet
• simp::types::MinHeap
• simp::types::NonEmptyVec
• simp::types::PathBuf
• simp::types::PrefixCounter
• simp::types::RawFnPtr
• simp::types::RewriteRule
• simp::types::RewriteRuleSet
• simp::types::SimpLemma
• simp::types::SimpLemmaSet
• simp::types::SimpResult
• simp::types::SimpleDag
• simp::types::SlidingSum
• simp::types::SmallMap
• simp::types::SparseVec
• simp::types::StackCalc
• simp::types::StatSummary
• simp::types::Stopwatch
• simp::types::StringPool
• simp::types::TokenBucket
• simp::types::TransformStat
• simp::types::TransitiveClosure
• simp::types::VersionedRecord
• simp::types::WindowIterator
• simp::types::WriteOnce
• struct_eta::types::EtaCanonMap
• struct_eta::types::EtaCategorizer
• struct_eta::types::EtaChangeEntry
• struct_eta::types::EtaChangeLog
• struct_eta::types::EtaDepthTracker
• struct_eta::types::EtaEqualityOracle
• struct_eta::types::EtaExpanded
• struct_eta::types::EtaGraph
• struct_eta::types::EtaLongChecker
• struct_eta::types::EtaNormRunSummary
• struct_eta::types::EtaNormalFormChecker
• struct_eta::types::EtaNormalizationPass
• struct_eta::types::EtaPassConfig
• struct_eta::types::EtaPassResult
• struct_eta::types::EtaRedex
• struct_eta::types::EtaRedexCollector
• struct_eta::types::EtaReduction
• struct_eta::types::EtaRewriteEngine
• struct_eta::types::EtaStateMachine
• struct_eta::types::EtaStats
• struct_eta::types::EtaUnificationHint
• struct_eta::types::FieldBoundsChecker
• struct_eta::types::FieldDescriptor
• struct_eta::types::InjectivityChecker
• struct_eta::types::KReductionTable
• struct_eta::types::ProjectionDescriptor
• struct_eta::types::ProjectionRewrite
• struct_eta::types::ProjectionRewriteSet
• struct_eta::types::RecordUpdate
• struct_eta::types::RecordUpdateBatch
• struct_eta::types::ShapeEquivalence
• struct_eta::types::SingletonKReducer
• struct_eta::types::StructFlatteningPass
• struct_eta::types::StructureDef
• struct_eta::types::StructureEta
• struct_eta::types::StructureRegistry
• subst::types::ConfigNode
• subst::types::FlatSubstitution
• subst::types::FocusStack
• subst::types::LabelSet
• subst::types::NonEmptyVec
• subst::types::PathBuf
• subst::types::RawFnPtr
• subst::types::RewriteRule
• subst::types::RewriteRuleSet
• subst::types::SimpleDag
• subst::types::SlidingSum
• subst::types::SmallMap
• subst::types::SparseVec
• subst::types::StackCalc
• subst::types::StatSummary
• subst::types::Stopwatch
• subst::types::StringPool
• subst::types::SubstStats
• subst::types::Substitution
• subst::types::TokenBucket
• subst::types::TransformStat
• subst::types::TransitiveClosure
• subst::types::VersionedRecord
• subst::types::WindowIterator
• subst::types::WriteOnce
• substitution::types::BitSet64
• substitution::types::BucketCounter
• substitution::types::ConfigNode
• substitution::types::Fixture
• substitution::types::FlatSubstitution
• substitution::types::FocusStack
• substitution::types::LabelSet
• substitution::types::MinHeap
• substitution::types::NonEmptyVec
• substitution::types::PathBuf
• substitution::types::PrefixCounter
• substitution::types::RawFnPtr
• substitution::types::RewriteRule
• substitution::types::RewriteRuleSet
• substitution::types::SimpleDag
• substitution::types::SlidingSum
• substitution::types::SmallMap
• substitution::types::SparseVec
• substitution::types::StackCalc
• substitution::types::StatSummary
• substitution::types::Stopwatch
• substitution::types::StringPool
• substitution::types::Substitution
• substitution::types::TokenBucket
• substitution::types::TransformStat
• substitution::types::TransitiveClosure
• substitution::types::VersionedRecord
• substitution::types::WindowIterator
• substitution::types::WriteOnce
• termination::types::ConfigNode
• termination::types::DetailedTerminationResult
• termination::types::Fixture
• termination::types::FlatSubstitution
• termination::types::FocusStack
• termination::types::LabelSet
• termination::types::MinHeap
• termination::types::NameIndex
• termination::types::NonEmptyVec
• termination::types::ParamInfo
• termination::types::PathBuf
• termination::types::PrefixCounter
• termination::types::RawFnPtr
• termination::types::RecCallInfo
• termination::types::RewriteRule
• termination::types::RewriteRuleSet
• termination::types::SimpleDag
• termination::types::SlidingSum
• termination::types::SmallMap
• termination::types::SparseVec
• termination::types::StackCalc
• termination::types::StatSummary
• termination::types::Stopwatch
• termination::types::StringPool
• termination::types::StringTrie
• termination::types::TerminationCache
• termination::types::TerminationChecker
• termination::types::TerminationResult
• termination::types::TokenBucket
• termination::types::TransformStat
• termination::types::TransitiveClosure
• termination::types::VersionedRecord
• termination::types::WindowIterator
• termination::types::WriteOnce
• trace::types::ConfigNode
• trace::types::FlatSubstitution
• trace::types::FocusStack
• trace::types::ForwardingTracer
• trace::types::LabelSet
• trace::types::NonEmptyVec
• trace::types::PathBuf
• trace::types::RawFnPtr
• trace::types::ReductionStep
• trace::types::RewriteRule
• trace::types::RewriteRuleSet
• trace::types::RingTracer
• trace::types::SimpleDag
• trace::types::SlidingSum
• trace::types::SmallMap
• trace::types::SparseVec
• trace::types::StackCalc
• trace::types::StatSummary
• trace::types::Stopwatch
• trace::types::StringPool
• trace::types::StringSink
• trace::types::TokenBucket
• trace::types::TraceEvent
• trace::types::TraceFilter
• trace::types::TraceSpan
• trace::types::Tracer
• trace::types::TracerStats
• trace::types::TransformStat
• trace::types::TransitiveClosure
• trace::types::VersionedRecord
• trace::types::WindowIterator
• trace::types::WriteOnce
• type_erasure::types::AnfConverter
• type_erasure::types::EraseConfig
• type_erasure::types::ErasedAst
• type_erasure::types::ErasedBetaReducer
• type_erasure::types::ErasedBitOps
• type_erasure::types::ErasedCallSite
• type_erasure::types::ErasedClosureEnv
• type_erasure::types::ErasedCodegen
• type_erasure::types::ErasedConstFolder
• type_erasure::types::ErasedConstantPool
• type_erasure::types::ErasedDCE
• type_erasure::types::ErasedEnv
• type_erasure::types::ErasedFlatApp
• type_erasure::types::ErasedInliner
• type_erasure::types::ErasedInterpreter
• type_erasure::types::ErasedLetChain
• type_erasure::types::ErasedLiveness
• type_erasure::types::ErasedMatchArm
• type_erasure::types::ErasedModule
• type_erasure::types::ErasedNormalizer
• type_erasure::types::ErasedOptimizer
• type_erasure::types::ErasedPrinter
• type_erasure::types::ErasedReachability
• type_erasure::types::ErasedRenamer
• type_erasure::types::ErasedScope
• type_erasure::types::ErasedSizeBound
• type_erasure::types::ErasedStack
• type_erasure::types::ErasedSubstMap
• type_erasure::types::ErasedTupleOps
• type_erasure::types::ErasedTypeMap
• type_erasure::types::ErasureContext
• type_erasure::types::ErasurePass
• type_erasure::types::ErasureStats
• type_erasure::types::PipelineRunner
• type_erasure::types::TypeEraser
• typeclasses::types::ClassEdge
• typeclasses::types::ConfigNode
• typeclasses::types::FlatSubstitution
• typeclasses::types::FocusStack
• typeclasses::types::Instance
• typeclasses::types::InstanceImpl
• typeclasses::types::LabelSet
• typeclasses::types::LayeredTypeClassRegistry
• typeclasses::types::Method
• typeclasses::types::MethodImpl
• typeclasses::types::NonEmptyVec
• typeclasses::types::NullResolver
• typeclasses::types::PathBuf
• typeclasses::types::RawFnPtr
• typeclasses::types::RegistrySnapshot
• typeclasses::types::RewriteRule
• typeclasses::types::RewriteRuleSet
• typeclasses::types::SimpleDag
• typeclasses::types::SlidingSum
• typeclasses::types::SmallMap
• typeclasses::types::SparseVec
• typeclasses::types::StackCalc
• typeclasses::types::StatSummary
• typeclasses::types::Stopwatch
• typeclasses::types::StringPool
• typeclasses::types::TokenBucket
• typeclasses::types::TransformStat
• typeclasses::types::TransitiveClosure
• typeclasses::types::TypeClass
• typeclasses::types::TypeClassRegistry
• typeclasses::types::TypeClassStats
• typeclasses::types::VersionedRecord
• typeclasses::types::WindowIterator
• typeclasses::types::WriteOnce
• universe::types::ConfigNode
• universe::types::FlatSubstitution
• universe::types::FocusStack
• universe::types::LabelSet
• universe::types::LevelComparisonTable
• universe::types::LevelNormalForm
• universe::types::NonEmptyVec
• universe::types::PathBuf
• universe::types::RawFnPtr
• universe::types::RewriteRule
• universe::types::RewriteRuleSet
• universe::types::SimpleDag
• universe::types::SlidingSum
• universe::types::SmallMap
• universe::types::SparseVec
• universe::types::StackCalc
• universe::types::StatSummary
• universe::types::Stopwatch
• universe::types::StringPool
• universe::types::TokenBucket
• universe::types::TransformStat
• universe::types::TransitiveClosure
• universe::types::UnivChecker
• universe::types::UnivConstraintSet
• universe::types::UnivPolySignature
• universe::types::UnivSatChecker
• universe::types::UniverseInstantiation
• universe::types::VersionedRecord
• universe::types::WindowIterator
• universe::types::WriteOnce
• whnf::types::ConfigNode
• whnf::types::Fixture
• whnf::types::FlatSubstitution
• whnf::types::FocusStack
• whnf::types::LabelSet
• whnf::types::MinHeap
• whnf::types::NonEmptyVec
• whnf::types::PathBuf
• whnf::types::PrefixCounter
• whnf::types::RawFnPtr
• whnf::types::ReductionBudget
• whnf::types::RewriteRule
• whnf::types::RewriteRuleSet
• whnf::types::SimpleDag
• whnf::types::SlidingSum
• whnf::types::SmallMap
• whnf::types::SparseVec
• whnf::types::StackCalc
• whnf::types::StatSummary
• whnf::types::Stopwatch
• whnf::types::StringPool
• whnf::types::TokenBucket
• whnf::types::TransformStat
• whnf::types::TransitiveClosure
• whnf::types::VersionedRecord
• whnf::types::WhnfCache
• whnf::types::WhnfCacheKey
• whnf::types::WhnfConfig
• whnf::types::WhnfDepthBudget
• whnf::types::WhnfStats
• whnf::types::WindowIterator
• whnf::types::WriteOnce

Enums

• DecisionNode
• Either2
• abstract::types::DecisionNode
• abstract::types::Either2
• abstract_interp::types::AbstractCmp
• abstract_interp::types::AlarmSeverity
• abstract_interp::types::BlockReachability
• abstract_interp::types::NullnessDomain
• abstract_interp::types::ParityDomain
• abstract_interp::types::SignDomain
• abstract_interp::types::SizeDomain
• abstract_interp::types::TerminationEvidence
• abstract_interp::types::TransferEffect
• abstract_interp::types::TrileanDomain
• alpha::types::DecisionNode
• alpha::types::Either2
• axiom::types::AxiomCategory
• axiom::types::AxiomSafety
• axiom::types::DecisionNode
• axiom::types::Either2
• bench_support::types::CompareResult
• bench_support::types::IterationPolicy
• bench_support::types::ThroughputUnit
• beta::types::DecisionNode
• beta::types::Either2
• builtin::types::BuiltinKind
• builtin::types::DecisionNode
• builtin::types::Either2
• cache::types::DecisionNode
• cache::types::Either2
• cache::types::SimplifiedExpr
• check::types::DecisionNode
• check::types::DeclKind
• check::types::Either2
• check::types::WellFormedResult
• congruence::types::CongrArgKind
• congruence::types::CongrProof
• congruence::types::DecisionNode
• congruence::types::Either2
• context::types::DecisionNode
• context::types::Either2
• conversion::types::ConvResult
• conversion::types::DecisionNode
• conversion::types::Either2
• declaration::types::ConstantInfo
• declaration::types::ConstantKind
• declaration::types::DeclAttr
• declaration::types::DeclKind
• declaration::types::DeclVisibility
• declaration::types::DefinitionSafety
• declaration::types::QuotKind
• def_eq::types::DecisionNode
• def_eq::types::Either2
• def_eq::types::ReductionStatus
• env::types::DecisionNode
• env::types::Declaration
• env::types::Either2
• env::types::EnvError
• equiv_manager::types::EquivProofTerm
• error::types::DecisionNode
• error::types::Either2
• error::types::ErrorCategory
• error::types::KernelError
• error::types::KernelPhase
• error::types::Severity
• eta::types::EtaOutcome
• eta::types::EtaStructure
• export::types::IntegrityCheckResult
• expr::types::BinderInfo
• expr::types::DecisionNode
• expr::types::Either2
• expr::types::Expr
• expr::types::Literal
• expr_cache::types::DecisionNode
• expr_cache::types::Either2
• expr_util::types::DecisionNode
• expr_util::types::Either2
• ffi::types::CallingConvention
• ffi::types::DecisionNode
• ffi::types::Either2
• ffi::types::FfiError
• ffi::types::FfiSafety
• ffi::types::FfiType
• ffi::types::FfiValue
• inductive::types::InductiveError
• infer::types::DecisionNode
• infer::types::Either2
• infer::types::TypeKind
• instantiate::types::DecisionNode
• instantiate::types::Either2
• level::types::DecisionNode
• level::types::Either2
• level::types::Level
• level::types::LevelConstraint
• match_compile::types::DecisionNode
• match_compile::types::DecisionTree
• match_compile::types::Either2
• match_compile::types::Pattern
• name::types::Name
• no_std_compat::types::ByteOrder
• no_std_compat::types::ErrorCode
• no_std_compat::types::OsResource
• no_std_compat::types::StaticStr
• normalize::types::DecisionNode
• normalize::types::Either2
• normalize::types::NormStrategy
• prettyprint::types::Doc
• prettyprint::types::IndentStyle
• prettyprint::types::PrettyDoc
• prettyprint::types::PrettyToken
• proof::types::DecisionNode
• proof::types::Either2
• proof::types::ProofComplexity
• quotient::types::EquivProperty
• quotient::types::QuotReductionKind
• quotient::types::QuotUsageKind
• reduce::types::DecisionNode
• reduce::types::Either2
• reduce::types::ReducibilityHint
• reduce::types::ReductionRule
• reduce::types::TransparencyMode
• reduction::types::DecisionNode
• reduction::types::Either2
• reduction::types::HeadForm
• reduction::types::RedexKind
• reduction::types::ReductionBound
• reduction::types::ReductionResult
• reduction::types::ReductionStrategy
• serial::types::MergeStrategy
• serial::types::MetadataValue
• serial::types::OleanError
• serial::types::SerialDecl
• simp::types::DecisionNode
• simp::types::Either2
• simp::types::SimpDirection
• struct_eta::types::CoherenceResult
• struct_eta::types::EtaCategory
• struct_eta::types::EtaChangeKind
• struct_eta::types::EtaLongStatus
• struct_eta::types::StructShape
• subst::types::DecisionNode
• subst::types::Either2
• substitution::types::DecisionNode
• substitution::types::Either2
• termination::types::DecisionNode
• termination::types::Either2
• termination::types::WfRelationKind
• trace::types::DecisionNode
• trace::types::Either2
• trace::types::ReductionRule
• trace::types::TraceCategory
• trace::types::TraceLevel
• type_erasure::types::ErasedDecl
• type_erasure::types::ErasedExpr
• type_erasure::types::ErasedExprExt
• type_erasure::types::ErasedHeapObj
• type_erasure::types::ErasedPattern
• type_erasure::types::ErasedValue
• typeclasses::types::DecisionNode
• typeclasses::types::Either2
• typeclasses::types::InstancePriority
• typeclasses::types::InstanceSearchResult
• universe::types::DecisionNode
• universe::types::Either2
• universe::types::UnivConstraint
• whnf::types::DecisionNode
• whnf::types::Either2
• whnf::types::StuckReason
• whnf::types::WhnfHead
• whnf::types::WhnfReductionOrder

Traits

• abstract_interp::functions::AbstractDomain
• arena::functions::ArenaAllocator
• def_eq::functions::ModuleMarker
• error::functions::KernelResultExt
• termination::functions::ModuleMarker
• type_erasure::functions::ErasedPass
• typeclasses::functions::InstanceResolver

Macros

• cfg_if_std
• name

Functions

• abstract::functions::abstract_fvars
• abstract::functions::abstract_fvars_ordered
• abstract::functions::abstract_single
• abstract::functions::apply_beta
• abstract::functions::bvars_in_range
• abstract::functions::cheap_beta_reduce
• abstract::functions::collect_app
• abstract::functions::collect_fvars
• abstract::functions::count_fvar_occurrences
• abstract::functions::distinct_const_count
• abstract::functions::is_closed_under
• abstract::functions::is_ground
• abstract::functions::lam_arity
• abstract::functions::let_abstract
• abstract::functions::let_abstract_many
• abstract::functions::max_bvar
• abstract::functions::mk_app
• abstract::functions::mk_forall
• abstract::functions::mk_lambda
• abstract::functions::pi_arity
• abstract::functions::rename_const
• abstract::functions::replace_nat_lit
• abstract::functions::shift_bvars
• abstract::functions::split_lam
• abstract::functions::split_pi
• abstract::functions::subst_fvar
• abstract::functions::topo_sort_fvars
• abstract_interp::functions::abstract_div
• abstract_interp::functions::narrow_env
• abstract_interp::functions::widen_env
• alpha::functions::all_alpha_equiv
• alpha::functions::alpha_class_rep
• alpha::functions::alpha_equiv
• alpha::functions::alpha_equiv_mod_levels
• alpha::functions::alpha_equiv_under_subst
• alpha::functions::alpha_hash
• alpha::functions::alpha_subst
• alpha::functions::apply_fvar_subst
• alpha::functions::bvar0_free
• alpha::functions::canonicalize
• alpha::functions::count_bvar0_occurrences
• alpha::functions::find_non_equiv_pair
• alpha::functions::free_fvars
• alpha::functions::fvar_occurs
• alpha::functions::lift
• alpha::functions::lower
• alpha::functions::rename_bvar
• alpha::functions::shift
• alpha::functions::structurally_equal
• alpha::functions::swap_bvars
• app_arity
• arena::functions::arena_alloc_array
• arena::functions::now_us
• axiom::functions::axiom_profile
• axiom::functions::axiom_summary
• axiom::functions::axioms_in_category
• axiom::functions::axioms_match
• axiom::functions::build_safety_report
• axiom::functions::classify_axiom
• axiom::functions::classify_axiom_category
• axiom::functions::count_definitions
• axiom::functions::direct_axiom_count
• axiom::functions::extract_axioms
• axiom::functions::has_axioms_of_category
• axiom::functions::has_unsafe_dependencies
• axiom::functions::is_axiom_free
• axiom::functions::is_prop_axiom
• axiom::functions::reachable_axioms
• axiom::functions::transitive_axiom_deps
• axiom::functions::validators_compatible
• bench_support::functions::calc_throughput
• bench_support::functions::compare_timings
• beta::functions::apply_k
• beta::functions::beta_applicative_order
• beta::functions::beta_equivalent
• beta::functions::beta_head_normalize
• beta::functions::beta_normal_order
• beta::functions::beta_normalize
• beta::functions::beta_normalize_fueled
• beta::functions::beta_normalize_with_stats
• beta::functions::beta_step
• beta::functions::beta_step_with_flag
• beta::functions::beta_under_binder
• beta::functions::beta_whnf
• beta::functions::collect_app_spine
• beta::functions::count_redexes
• beta::functions::count_reduction_steps
• beta::functions::estimate_reduction_depth
• beta::functions::eta_expand
• beta::functions::eta_reduce
• beta::functions::has_let
• beta::functions::is_beta_normal
• beta::functions::is_eta_reducible
• beta::functions::is_whnf
• beta::functions::mk_beta_redex
• beta::functions::mk_compose
• beta::functions::mk_const_fn
• beta::functions::mk_i_combinator
• beta::functions::mk_identity
• beta::functions::mk_k_combinator
• beta::functions::mk_multi_beta_redex
• beta::functions::reduce_app_spine
• beta::functions::reduce_lets
• build_lam_from_binders
• build_pi_from_binders
• builtin::functions::all_builtin_names
• builtin::functions::builtin_count
• builtin::functions::builtin_ctor_count
• builtin::functions::builtin_is_prop
• builtin::functions::builtin_is_recursive
• builtin::functions::builtin_universe_level
• builtin::functions::classify_builtin
• builtin::functions::core_builtin_infos
• builtin::functions::init_builtin_env
• builtin::functions::is_builtin
• builtin::functions::is_logical_connective
• builtin::functions::is_nat_op
• builtin::functions::is_primitive_value
• builtin::functions::is_string_op
• builtin::functions::lean4_name
• builtin::functions::verify_builtins
• cache::functions::fnv1a_hash
• check::functions::check_constant_info
• check::functions::check_constant_infos
• check::functions::check_declaration
• check::functions::check_declarations
• check::functions::check_declarations_collect_errors
• check::functions::check_declarations_with_stats
• check::functions::check_dependencies_exist
• check::functions::declaration_dependencies
• check::functions::format_batch_result
• check::functions::format_decl_summary
• check::functions::has_unique_univ_params
• check::functions::is_structurally_valid_expr
• check::functions::is_valid_decl_name
• check::functions::summarize_declaration
• check::functions::univ_params_compatible
• check::functions::verify_environment_integrity
• collect_const_names
• collect_fvars
• collect_literals
• congruence::functions::all_hypotheses_trivial
• congruence::functions::compatible_heads
• congruence::functions::generate_congr_hypotheses
• congruence::functions::is_simple_head
• congruence::functions::mk_congr_theorem
• congruence::functions::mk_congr_theorem_with_fixed
• const_name
• contains_bvar
• context::functions::collect_fvars
• context::functions::count_fvar
• context::functions::fvar_occurs
• context::functions::name_gen::fresh
• context::functions::name_gen::greek
• context::functions::name_gen::hyp
• context::functions::name_gen::mvar
• context::functions::rename_fvar
• conversion::functions::alpha_similar
• conversion::functions::bounded_conversion
• conversion::functions::check_conversion
• conversion::functions::contains_subterm
• conversion::functions::conversion_diff
• conversion::functions::convertibility_score
• conversion::functions::count_free_vars
• conversion::functions::def_eq_with_mode
• conversion::functions::expr_depth
• conversion::functions::expr_size
• conversion::functions::exprs_equal
• conversion::functions::is_atomic
• conversion::functions::is_beta_normal
• conversion::functions::is_eta_equal
• conversion::functions::is_leaf
• conversion::functions::is_transparency_neutral
• conversion::functions::levels_def_eq
• conversion::functions::same_head
• conversion::functions::structural_distance
• conversion::functions::syntactic_eq
• count_apps
• count_lam_binders
• count_pi_binders
• count_sorts
• declaration::functions::check_level_params_consistent
• declaration::functions::collect_level_params_in_expr
• declaration::functions::instantiate_level_params
• declaration::functions::now_us
• def_eq::functions::closest_match
• def_eq::functions::format_name_list
• def_eq::functions::is_def_eq_args
• def_eq::functions::is_def_eq_simple
• def_eq::functions::is_def_eq_with_mode
• def_eq::functions::levenshtein_distance
• def_eq::functions::module_err
• def_eq::functions::syntactic_eq
• env::functions::constants_with_prefix
• env::functions::contains_any
• env::functions::env_stats
• env::functions::filter_environment
• env::functions::merge_environments
• env::functions::missing_names
• env::functions::present_names
• equiv_manager::functions::compute_equiv_classes
• equiv_manager::functions::compute_representatives
• equiv_manager::functions::find_classes
• equiv_manager::functions::now_us
• equiv_manager::functions::transitive_closure
• error::functions::collect_unknown_constants
• error::functions::format_error_panel
• error::functions::has_universe_errors
• error::functions::summarise_error
• error::functions::try_kernel
• eta::functions::app_depth
• eta::functions::apply_bvars
• eta::functions::arity
• eta::functions::beta_reduce_full
• eta::functions::beta_reduce_one
• eta::functions::binder_depth
• eta::functions::collect_app_spine
• eta::functions::contains_bvar
• eta::functions::count_bvar
• eta::functions::eta_contract
• eta::functions::eta_contract_full
• eta::functions::eta_def_eq
• eta::functions::eta_equiv
• eta::functions::eta_equiv_depth
• eta::functions::eta_expand
• eta::functions::eta_expand_implicit
• eta::functions::eta_expand_pi
• eta::functions::eta_expand_to
• eta::functions::eta_expand_with_ty
• eta::functions::eta_head
• eta::functions::eta_normalize
• eta::functions::eta_normalize_tracked
• eta::functions::expr_is_closed
• eta::functions::expr_structure_desc
• eta::functions::is_beta_redex
• eta::functions::is_closed
• eta::functions::is_closed_at
• eta::functions::is_eta_expandable
• eta::functions::is_eta_long
• eta::functions::is_eta_redex
• eta::functions::is_identity_lambda
• eta::functions::is_lambda_free
• eta::functions::is_simple_app
• eta::functions::lam_to_pi
• eta::functions::mk_app_spine
• eta::functions::node_count
• eta::functions::normal_eq
• eta::functions::normalize_full
• eta::functions::outer_lambda_depth
• eta::functions::peel_lambdas
• eta::functions::peel_pis
• eta::functions::pi_depth
• eta::functions::rebuild_lam
• eta::functions::rebuild_pi
• eta::functions::reduce_let
• eta::functions::reduce_lets
• eta::functions::rewrite_with_rules
• eta::functions::shift_down
• eta::functions::shift_up
• eta::functions::structural_hash
• eta::functions::subst_bvar
• eta::functions::subst_bvar_shifted
• eta::functions::wrap_in_lambdas
• export::functions::check_bytes_integrity
• export::functions::check_module_integrity
• export::functions::deserialize_module
• export::functions::deserialize_module_header
• export::functions::diff_modules
• export::functions::export_environment
• export::functions::import_module
• export::functions::serialize_module
• expr::functions::app_args
• expr::functions::app_head
• expr::functions::count_occurrences
• expr::functions::mk_and
• expr::functions::mk_arrow
• expr::functions::mk_arrows
• expr::functions::mk_const
• expr::functions::mk_eq
• expr::functions::mk_lam_many
• expr::functions::mk_let
• expr::functions::mk_not
• expr::functions::mk_or
• expr::functions::mk_pi_many
• expr::functions::mk_refl
• expr::functions::prop
• expr::functions::same_head
• expr::functions::subst_expr
• expr::functions::type0
• expr::functions::type1
• expr_head
• expr_size
• expr_util::functions::app
• expr_util::functions::bvar
• expr_util::functions::collect_consts
• expr_util::functions::collect_fvars
• expr_util::functions::count_lambdas
• expr_util::functions::count_pis
• expr_util::functions::decompose_lam
• expr_util::functions::decompose_let
• expr_util::functions::decompose_pi
• expr_util::functions::decompose_proj
• expr_util::functions::expr_weight
• expr_util::functions::for_each_expr
• expr_util::functions::get_app_args
• expr_util::functions::get_app_fn
• expr_util::functions::get_app_fn_args
• expr_util::functions::get_app_num_args
• expr_util::functions::get_bvar_idx
• expr_util::functions::get_const_levels
• expr_util::functions::get_const_name
• expr_util::functions::get_fvar_id
• expr_util::functions::get_nth_arg
• expr_util::functions::get_sort_level
• expr_util::functions::has_any_fvar
• expr_util::functions::has_fvar
• expr_util::functions::has_level_mvar
• expr_util::functions::has_level_param
• expr_util::functions::has_loose_bvar
• expr_util::functions::has_loose_bvar_ge
• expr_util::functions::has_loose_bvars
• expr_util::functions::is_app
• expr_util::functions::is_app_of
• expr_util::functions::is_app_of_fvar
• expr_util::functions::is_bvar
• expr_util::functions::is_const
• expr_util::functions::is_fvar
• expr_util::functions::is_lambda
• expr_util::functions::is_let
• expr_util::functions::is_literal
• expr_util::functions::is_pi
• expr_util::functions::is_proj
• expr_util::functions::is_prop
• expr_util::functions::is_simple
• expr_util::functions::is_sort
• expr_util::functions::is_type0
• expr_util::functions::lam
• expr_util::functions::level_has_mvar
• expr_util::functions::lift_loose_bvars
• expr_util::functions::mk_app
• expr_util::functions::mk_app_range
• expr_util::functions::mk_arrow
• expr_util::functions::mk_lam_n
• expr_util::functions::mk_pi_n
• expr_util::functions::mk_prop
• expr_util::functions::mk_type
• expr_util::functions::mk_type0
• expr_util::functions::occurs_const
• expr_util::functions::pi
• expr_util::functions::prop
• expr_util::functions::replace_expr
• expr_util::functions::sort
• expr_util::functions::strip_lambdas
• expr_util::functions::strip_pis
• expr_util::functions::type0
• expr_util::functions::var
• has_let_binders
• has_metavars
• has_projections
• inductive::functions::check_inductive
• inductive::functions::constructor_field_counts
• inductive::functions::is_enum_inductive
• inductive::functions::is_singleton_inductive
• inductive::functions::mk_bool_inductive
• inductive::functions::mk_empty_inductive
• inductive::functions::mk_nat_inductive
• inductive::functions::mk_unit_inductive
• inductive::functions::recursor_name
• inductive::functions::reduce_recursor
• infer::functions::classify_expr
• infer::functions::is_pi
• infer::functions::is_prop
• infer::functions::is_sort
• infer::functions::pi_components
• infer::functions::pi_sort
• instantiate::functions::abstract_fvar
• instantiate::functions::abstract_fvars
• instantiate::functions::beta_apply
• instantiate::functions::beta_reduce_head
• instantiate::functions::beta_reduce_once
• instantiate::functions::has_loose_bvars
• instantiate::functions::instantiate_expr_mvars
• instantiate::functions::instantiate_many
• instantiate::functions::instantiate_one
• instantiate::functions::instantiate_rev
• instantiate::functions::instantiate_type_lparams
• instantiate::functions::is_whnf_simple
• instantiate::functions::lift_bvars
• instantiate::functions::max_loose_bvar
• instantiate::functions::subst_fvar
• instantiate::functions::subst_fvars
• instantiate::functions::unfold_all_lets
• instantiate::functions::unfold_let_one
• is_app
• is_app_of
• is_closed
• is_const
• is_eta_reducible
• is_ground
• is_lam
• is_literal
• is_pi
• is_sort
• kernel_version
• level::functions::collect_level_mvars
• level::functions::collect_level_params
• level::functions::dedup_levels
• level::functions::eval_ground_level
• level::functions::flatten_max
• level::functions::imax_fold
• level::functions::instantiate_level
• level::functions::instantiate_level_mvars
• level::functions::is_definitely_succ
• level::functions::is_equivalent
• level::functions::is_geq
• level::functions::is_ground
• level::functions::is_leq
• level::functions::is_numeral
• level::functions::level_add
• level::functions::level_max3
• level::functions::level_min
• level::functions::max_of_slice
• level::functions::normalize
• level::functions::to_offset
• level::functions::type0_level
• level::functions::type1_level
• level::functions::type_level
• match_compile::functions::compute_match_stats
• match_compile::functions::count_decision_tree_leaves
• match_compile::functions::count_pattern_bindings
• match_compile::functions::decision_tree_depth
• match_compile::functions::flatten_or_patterns
• match_compile::functions::is_irrefutable
• match_compile::functions::is_irrefutable_pattern
• match_compile::functions::pattern_binders
• match_compile::functions::pattern_constructor
• match_compile::functions::pattern_depth
• match_compile::functions::pattern_subpatterns
• match_compile::functions::referenced_arm_indices
• max_binder_depth
• max_bvar_index
• mk_app
• mk_app_spine
• mk_lam
• mk_lam_chain
• mk_nat_lit
• mk_pi
• mk_pi_chain
• mk_prop
• mk_sort
• mk_string_lit
• mk_type0
• mk_type1
• name::functions::direct_children
• name::functions::longest_common_prefix
• name::functions::now_us
• name::functions::share_namespace
• no_std_compat::functions::bool_to_platform_result
• no_std_compat::functions::os_bytes_to_string
• no_std_compat::functions::str_to_os_bytes
• normalize::functions::alpha_eq
• normalize::functions::alpha_eq_env
• normalize::functions::count_reduction_steps
• normalize::functions::evaluate
• normalize::functions::head_normal_form
• normalize::functions::is_in_whnf
• normalize::functions::is_normal_form
• normalize::functions::normalize
• normalize::functions::normalize_binders
• normalize::functions::normalize_env
• normalize::functions::normalize_fully
• normalize::functions::normalize_many
• normalize::functions::normalize_many_env
• normalize::functions::normalize_selective
• normalize::functions::normalize_types
• normalize::functions::normalize_whnf
• normalize::functions::normalize_with_stats
• normalize::functions::normalize_with_strategy
• normalize::functions::reduce_n_steps
• prettyprint::functions::colorize
• prettyprint::functions::expr_summary
• prettyprint::functions::expr_to_doc
• prettyprint::functions::is_simple_name
• prettyprint::functions::now_us
• prettyprint::functions::print_expr
• prettyprint::functions::print_expr_ascii
• prettyprint::functions::print_expr_with_config
• prettyprint::functions::print_level
• prettyprint::functions::print_name_str
• proof::functions::axiom_dependencies
• proof::functions::classify_proof
• proof::functions::collect_axiom_deps
• proof::functions::count_const_occurrences
• proof::functions::is_closed_term
• proof::functions::is_proof_irrelevant
• proof::functions::proof_effort
• proof::functions::same_proof_shape
• quotient::functions::all_quot_mk
• quotient::functions::build_quot_lift
• quotient::functions::build_quot_mk
• quotient::functions::build_quot_sound
• quotient::functions::build_quot_type
• quotient::functions::check_equivalence_relation
• quotient::functions::check_quot_usage
• quotient::functions::collect_quot_mk
• quotient::functions::contains_quot_lift
• quotient::functions::count_quot_mk
• quotient::functions::extract_quot_lift_args
• quotient::functions::is_eq_relation
• quotient::functions::is_full_quot_lift
• quotient::functions::is_identity_relation
• quotient::functions::is_quot_const
• quotient::functions::is_quot_mk
• quotient::functions::is_quot_normal
• quotient::functions::is_quot_sound
• quotient::functions::is_quot_type_expr
• quotient::functions::lift_map
• quotient::functions::quot_const_arity
• quotient::functions::quot_eq
• quotient::functions::quot_lift_eq_proof
• quotient::functions::quot_mk_arg
• quotient::functions::quot_mk_def_eq
• quotient::functions::quot_mk_name_for
• quotient::functions::quot_type_doc
• quotient::functions::reduce_quot_ind
• quotient::functions::reduce_quot_lift
• quotient::functions::standard_quot_consts
• quotient::functions::strip_quot_mk
• quotient::functions::try_reduce_quot
• quotient::functions::try_reduce_quot_full
• quotient::functions::validate_quotient_type
• reduce::functions::app_arity
• reduce::functions::eval_nat_binop
• reduce::functions::eval_nat_cmp
• reduce::functions::head_of
• reduce::functions::is_whnf
• reduce::functions::reduce_nat_op
• reduction::functions::alpha_equiv
• reduction::functions::are_convertible
• reduction::functions::build_reduction_trace
• reduction::functions::classify_head
• reduction::functions::count_beta_redexes
• reduction::functions::count_reduction_steps
• reduction::functions::expr_depth
• reduction::functions::expr_fingerprint
• reduction::functions::expr_size
• reduction::functions::find_redexes
• reduction::functions::is_normal_form
• reduction::functions::reduce_bounded
• reduction::functions::reduce_head
• reduction::functions::reduce_with_strategy
• reduction::functions::try_reduce_step
• replace_const
• serial::functions::blobs_equal
• serial::functions::count_by_kind
• serial::functions::decode_decl
• serial::functions::dedup_decls
• serial::functions::deserialize_decl_names
• serial::functions::deserialize_decls
• serial::functions::encode_decl
• serial::functions::filter_by_kind
• serial::functions::find_by_prefix
• serial::functions::fnv1a_64
• serial::functions::from_hex
• serial::functions::group_by_namespace
• serial::functions::has_valid_magic
• serial::functions::merge_decls
• serial::functions::peek_decl_count
• serial::functions::peek_version
• serial::functions::read_bools
• serial::functions::read_oleanc_file
• serial::functions::serialize_decl_names
• serial::functions::serialize_decls
• serial::functions::serialized_decl_size
• serial::functions::serialized_string_size
• serial::functions::sort_decls_by_name
• serial::functions::to_hex
• serial::functions::total_serialized_size
• serial::functions::with_context
• serial::functions::write_bools
• serial::functions::write_name_table_section
• serial::functions::write_oleanc_file
• simp::functions::alpha_eq
• simp::functions::contains_bvar
• simp::functions::decompose_app
• simp::functions::eta_reduce
• simp::functions::eval_nat
• simp::functions::expr_depth
• simp::functions::expr_size
• simp::functions::fold_nat_constants
• simp::functions::free_vars
• simp::functions::is_app_of
• simp::functions::is_closed
• simp::functions::is_false_expr
• simp::functions::is_nat_lit
• simp::functions::is_prop
• simp::functions::is_succ
• simp::functions::is_true
• simp::functions::is_zero
• simp::functions::mk_app
• simp::functions::normalize
• simp::functions::rewrite_all
• simp::functions::rewrite_once
• simp::functions::simp_congruence
• simp::functions::simp_with_trace
• simp::functions::simplify
• simp::functions::simplify_bounded
• simp::functions::succ_of
• strip_lam_binders
• strip_pi_binders
• subst::functions::abstract_expr
• subst::functions::apply_args
• subst::functions::beta_reduce_head
• subst::functions::build_subst_map
• subst::functions::collect_loose_bvar_indices
• subst::functions::count_free_occurrences
• subst::functions::count_lambdas
• subst::functions::count_pis
• subst::functions::expr_contains_fvar
• subst::functions::free_vars
• subst::functions::instantiate
• subst::functions::instantiate_many
• subst::functions::instantiate_tracked
• subst::functions::is_lambda
• subst::functions::is_whnf_beta
• subst::functions::occurs_free
• subst::functions::open_binder
• subst::functions::parallel_subst
• subst::functions::parallel_subst_tracked
• subst::functions::peel_lambdas
• subst::functions::shift_bvars
• subst::functions::subst_fvar
• subst::functions::substitute_fvars
• subst::functions::try_beta_reduce
• substitution::functions::abstract_fvar
• substitution::functions::abstract_fvars_ordered
• substitution::functions::alpha_eq
• substitution::functions::close_with_lambdas
• substitution::functions::close_with_pis
• substitution::functions::collect_consts
• substitution::functions::collect_fvars
• substitution::functions::count_bvar
• substitution::functions::count_fvar
• substitution::functions::expr_depth
• substitution::functions::expr_size
• substitution::functions::has_bvar
• substitution::functions::has_fvar
• substitution::functions::instantiate
• substitution::functions::is_closed
• substitution::functions::is_ground
• substitution::functions::lift
• substitution::functions::lower
• substitution::functions::rename_binder
• substitution::functions::subst
• substitution::functions::subst_const
• substitution::functions::subst_fvars
• syntactically_equal
• termination::functions::closest_match
• termination::functions::format_name_list
• termination::functions::has_obvious_nontermination
• termination::functions::levenshtein_distance
• termination::functions::module_err
• termination::functions::try_structural_certificate
• trace::functions::count_filtered
• trace::functions::count_matching
• trace::functions::def_eq_event
• trace::functions::def_eq_event_at
• trace::functions::elab_event
• trace::functions::error_event
• trace::functions::filter_events
• trace::functions::filtered_events
• trace::functions::has_message_containing
• trace::functions::infer_event
• trace::functions::merge_tracers
• trace::functions::reduce_event
• trace::functions::replay_into_sink
• trace::functions::simp_event
• trace::functions::summarize_reductions
• trace::functions::tactic_event
• trace::functions::typeclass_event
• trace::functions::unify_event
• trace::functions::unique_categories
• trace::functions::warn_event
• type_erasure::functions::build_apps
• type_erasure::functions::collect_consts
• type_erasure::functions::count_apps
• type_erasure::functions::count_free_vars
• type_erasure::functions::flatten_apps
• type_erasure::functions::has_free_bvar
• type_erasure::functions::lambda_depth
• type_erasure::functions::pretty_print_erased
• type_erasure::functions::subst_bvar0
• typeclasses::functions::all_method_pairs
• typeclasses::functions::build_class_hierarchy
• typeclasses::functions::build_method_projection
• typeclasses::functions::class_has_instance
• typeclasses::functions::class_name_of_constraint
• typeclasses::functions::classes_equal
• typeclasses::functions::classes_without_instances
• typeclasses::functions::complete_instances
• typeclasses::functions::default_registry
• typeclasses::functions::describe_registry
• typeclasses::functions::find_method_impl
• typeclasses::functions::has_higher_priority
• typeclasses::functions::instance_is_complete
• typeclasses::functions::instance_subsumes
• typeclasses::functions::instance_summary
• typeclasses::functions::instances_compatible
• typeclasses::functions::instances_match
• typeclasses::functions::is_ancestor
• typeclasses::functions::is_class_constraint
• typeclasses::functions::is_prop_class
• typeclasses::functions::merge_registries
• typeclasses::functions::methods_of
• typeclasses::functions::register_add
• typeclasses::functions::register_heq
• typeclasses::functions::register_inhabited
• typeclasses::functions::register_marker
• typeclasses::functions::register_mul
• typeclasses::functions::shared_methods
• typeclasses::functions::total_method_impls
• typeclasses::functions::transitive_supers
• typeclasses::functions::typeclass_summary
• typeclasses::functions::validate_registry
• unfold_app
• universe::functions::add_succ_n
• universe::functions::add_succs
• universe::functions::collect_level_params
• universe::functions::count_succ_depth
• universe::functions::count_succs
• universe::functions::eval_closed_level
• universe::functions::format_level
• universe::functions::instantiate_levels
• universe::functions::is_imax_level
• universe::functions::is_max_level
• universe::functions::is_prop_level
• universe::functions::is_valid_instantiation
• universe::functions::level_imax
• universe::functions::level_max
• universe::functions::level_max_many
• universe::functions::level_succ
• universe::functions::level_to_nat
• universe::functions::parse_level_str
• universe::functions::peel_succs
• universe::functions::pi_type_level
• universe::functions::prop_level
• universe::functions::same_level_shape
• universe::functions::sort_type_level
• universe::functions::substitute_level_param
• universe::functions::type0_level
• universe::functions::type1_level
• whnf::functions::app_arity
• whnf::functions::collect_pi_telescope
• whnf::functions::collect_pi_telescope_env
• whnf::functions::count_nodes
• whnf::functions::expr_depth
• whnf::functions::is_whnf
• whnf::functions::normalize_full
• whnf::functions::normalize_head
• whnf::functions::spine_of
• whnf::functions::stuck_reason
• whnf::functions::whnf
• whnf::functions::whnf_as_fvar
• whnf::functions::whnf_as_pi
• whnf::functions::whnf_as_pi_env
• whnf::functions::whnf_as_sort
• whnf::functions::whnf_budgeted
• whnf::functions::whnf_env
• whnf::functions::whnf_head_is_const
• whnf::functions::whnf_heads_match
• whnf::functions::whnf_is_const
• whnf::functions::whnf_is_fvar
• whnf::functions::whnf_is_lambda
• whnf::functions::whnf_is_lit
• whnf::functions::whnf_is_pi
• whnf::functions::whnf_is_sort
• whnf::functions::whnf_spine
• whnf::functions::whnf_spine_env

Type Aliases

• congruence::functions::TermIdx
• def_eq::functions::ModuleResult
• error::functions::KernelResult
• no_std_compat::functions::PlatformResult
• serial::functions::SerialResult
• subst::functions::SubstMap
• termination::functions::ModuleResult

Constants

• KERNEL_VERSION
• def_eq::functions::MODULE_VERSION
• export::functions::FORMAT_VERSION
• export::functions::MAGIC_NUMBER
• level::functions::PROP_LEVEL
• no_std_compat::functions::STANDARD_SECTIONS
• prettyprint::functions::ansi::BLUE
• prettyprint::functions::ansi::BOLD
• prettyprint::functions::ansi::CYAN
• prettyprint::functions::ansi::DIM
• prettyprint::functions::ansi::GREEN
• prettyprint::functions::ansi::MAGENTA
• prettyprint::functions::ansi::RED
• prettyprint::functions::ansi::RESET
• prettyprint::functions::ansi::YELLOW
• serial::functions::kind_tags::AXIOM
• serial::functions::kind_tags::DEFINITION
• serial::functions::kind_tags::INDUCTIVE
• serial::functions::kind_tags::OPAQUE
• serial::functions::kind_tags::OTHER
• serial::functions::kind_tags::THEOREM
• serial::functions::section_tags::CHECKSUM
• serial::functions::section_tags::DEBUG_INFO
• serial::functions::section_tags::DECLARATIONS
• serial::functions::section_tags::EXPORT_LIST
• serial::functions::section_tags::NAME_TABLE
• serial::functions::section_tags::UNIVERSE_LEVELS
• termination::functions::MODULE_VERSION