List of all items
Structs
- host::LeanBracketedDeclarationInfo
- host::LeanBracketedImportRequest
- host::LeanBracketedImportResult
- host::LeanBracketedRejectedOperation
- host::LeanCancellationToken
- host::LeanCapabilities
- host::LeanDeclarationFilter
- host::LeanHost
- host::LeanImportProfilerOptions
- host::LeanImportStats
- host::LeanProgressEvent
- host::LeanSession
- host::LeanSourceRange
- host::SessionStats
- host::declaration_search::DeclarationFlags
- host::declaration_search::DeclarationInspection
- host::declaration_search::DeclarationInspectionBudgets
- host::declaration_search::DeclarationInspectionFields
- host::declaration_search::DeclarationInspectionRequest
- host::declaration_search::DeclarationProofSearchFacts
- host::declaration_search::DeclarationRenderedInfo
- host::declaration_search::DeclarationSearchBias
- host::declaration_search::DeclarationSearchFacts
- host::declaration_search::DeclarationSearchPruning
- host::declaration_search::DeclarationSearchRequest
- host::declaration_search::DeclarationSearchResult
- host::declaration_search::DeclarationSearchRow
- host::declaration_search::DeclarationSearchTimings
- host::declaration_search::LeanDerivedWorkFacts
- host::elaboration::LeanDiagnostic
- host::elaboration::LeanElabFailure
- host::elaboration::LeanElabOptions
- host::elaboration::LeanPosition
- host::evidence::LeanEvidence
- host::evidence::ProofSummary
- host::meta::LeanMetaOptions
- host::meta::LeanMetaService
- host::pool::PoolStats
- host::pool::PooledSession
- host::pool::SessionPool
- host::pool::SessionPoolConfig
- host::pool::SessionPoolMemoryPolicy
- host::process::DeclarationOutlineResult
- host::process::DeclarationTargetInfo
- host::process::DeclarationVerificationBatchItem
- host::process::DeclarationVerificationBatchRequest
- host::process::DeclarationVerificationBatchRow
- host::process::DeclarationVerificationFacts
- host::process::DeclarationVerificationRequest
- host::process::LocalInfo
- host::process::ModuleQueryBatchEnvelope
- host::process::ModuleQueryCacheFacts
- host::process::ModuleQueryCachePolicy
- host::process::ModuleQueryOutputBudgets
- host::process::ModuleQueryTimings
- host::process::ModuleSnapshotCacheClearResult
- host::process::ModuleSourceSpan
- host::process::NameRefNode
- host::process::ProofAttemptEnvelope
- host::process::ProofAttemptRequest
- host::process::ProofAttemptRow
- host::process::ProofBoundaryCandidate
- host::process::ProofCandidate
- host::process::ProofPositionSummary
- host::process::ProofStateInfo
- host::process::ReferencesResult
- host::process::RenderedInfo
Enums
- host::LeanImportLevel
- host::LeanImportProfileMode
- host::LeanSessionImportProfile
- host::declaration_search::DeclarationInspectionResult
- host::declaration_search::DeclarationNameMatch
- host::declaration_search::DeclarationSearchScope
- host::elaboration::LeanSeverity
- host::evidence::EvidenceStatus
- host::evidence::LeanKernelOutcome
- host::meta::LeanMetaResponse
- host::meta::LeanMetaTransparency
- host::meta::MetaCallStatus
- host::pool::SessionPoolKeyMissReason
- host::process::DeclarationTargetResult
- host::process::DeclarationVerificationBatchOutcome
- host::process::DeclarationVerificationOutcome
- host::process::DeclarationVerificationStatus
- host::process::DeclarationVerificationTarget
- host::process::GoalAtResult
- host::process::ModuleQuery
- host::process::ModuleQueryBatchCachedOutcome
- host::process::ModuleQueryBatchItem
- host::process::ModuleQueryBatchOutcome
- host::process::ModuleQueryBatchResult
- host::process::ModuleQueryCacheStatus
- host::process::ModuleQueryOutcome
- host::process::ModuleQueryResult
- host::process::ModuleQuerySelector
- host::process::ProofAttemptOutcome
- host::process::ProofAttemptStatus
- host::process::ProofEditTarget
- host::process::ProofPositionSelector
- host::process::ProofStateResult
- host::process::SorryPolicy
- host::process::SurroundingDeclarationResult
- host::process::TypeAtResult
Traits
Functions
- host::meta::heartbeat_burn
- host::meta::infer_type
- host::meta::is_def_eq
- host::meta::pp_expr
- host::meta::whnf
Constants
- LEAN_DIAGNOSTIC_BYTE_LIMIT_DEFAULT
- LEAN_DIAGNOSTIC_BYTE_LIMIT_MAX
- LEAN_HEARTBEAT_LIMIT_DEFAULT
- LEAN_HEARTBEAT_LIMIT_MAX
- host::elaboration::LEAN_DIAGNOSTIC_BYTE_LIMIT_DEFAULT
- host::elaboration::LEAN_DIAGNOSTIC_BYTE_LIMIT_MAX
- host::elaboration::LEAN_HEARTBEAT_LIMIT_DEFAULT
- host::elaboration::LEAN_HEARTBEAT_LIMIT_MAX
- host::evidence::LEAN_PROOF_SUMMARY_BYTE_LIMIT