Skip to main content

lean_rs_host/host/process/
mod.rs

1//! Bounded module-query projection capability on [`crate::LeanSession`].
2//!
3//! [`crate::LeanSession::process_module_query`] takes a full Lean source
4//! file plus a [`ModuleQuery`]. Lean parses the header, elaborates the
5//! body, performs the requested cursor/reference/diagnostic projection,
6//! and returns only that bounded result. Raw whole-file `InfoTree`
7//! projections do not cross the FFI boundary.
8
9mod query;
10
11pub use self::query::{
12    DeclarationOutlineResult, DeclarationTargetInfo, DeclarationTargetResult, DeclarationVerificationBatchItem,
13    DeclarationVerificationBatchOutcome, DeclarationVerificationBatchRequest, DeclarationVerificationBatchRow,
14    DeclarationVerificationFacts, DeclarationVerificationOutcome, DeclarationVerificationRequest,
15    DeclarationVerificationStatus, DeclarationVerificationTarget, GoalAtResult, LocalInfo, ModuleQuery,
16    ModuleQueryBatchCachedOutcome, ModuleQueryBatchEnvelope, ModuleQueryBatchItem, ModuleQueryBatchOutcome,
17    ModuleQueryBatchResult, ModuleQueryCacheFacts, ModuleQueryCachePolicy, ModuleQueryCacheStatus, ModuleQueryOutcome,
18    ModuleQueryOutputBudgets, ModuleQueryResult, ModuleQuerySelector, ModuleQueryTimings,
19    ModuleSnapshotCacheClearResult, ModuleSourceSpan, NameRefNode, ProofAttemptEnvelope, ProofAttemptOutcome,
20    ProofAttemptRequest, ProofAttemptRow, ProofAttemptStatus, ProofBoundaryCandidate, ProofCandidate, ProofEditTarget,
21    ProofPositionSelector, ProofPositionSummary, ProofStateInfo, ProofStateResult, ReferencesResult, RenderedInfo,
22    SorryPolicy, SurroundingDeclarationResult, TypeAtResult,
23};