Module process 

Bounded module-query projection capability on crate::LeanSession.

crate::LeanSession::process_module_query takes a full Lean source file plus a ModuleQuery. Lean parses the header, elaborates the body, performs the requested cursor/reference/diagnostic projection, and returns only that bounded result. Raw whole-file InfoTree projections do not cross the FFI boundary.

Structs

DeclarationOutlineResult

Result for ModuleQuerySelector::DeclarationOutline.

DeclarationTargetInfo

Source metadata for the declaration surrounding a proof-agent query.

DeclarationVerificationBatchItem

One target inside a batch declaration-verification request.

DeclarationVerificationBatchRequest

Bounded request to verify several declarations in one source snapshot.

DeclarationVerificationBatchRow

One ordered row inside a batch declaration-verification result.

DeclarationVerificationFacts

Bounded facts returned by declaration verification.

DeclarationVerificationRequest

Bounded request to verify one declaration in a source snapshot.

LocalInfo

One rendered local declaration in a proof-state result.

ModuleQueryBatchEnvelope

Successful batch selector envelope.

ModuleQueryCacheFacts

Cache and timing facts attached to cached batched module-query outcomes.

ModuleQueryCachePolicy

Cache policy passed to the Lean-side module snapshot cache.

ModuleQueryOutputBudgets

Explicit byte budgets for a batched module query.

ModuleQueryTimings

Phase timings for cached batched module queries, in microseconds.

ModuleSnapshotCacheClearResult

Result of clearing the Lean-side module snapshot cache.

ModuleSourceSpan

Source span in the original file. Positions are 1-based.

NameRefNode

One identifier occurrence the elaborator recorded.

ProofAttemptEnvelope

Envelope for a bounded proof attempt.

ProofAttemptRequest

Bounded request to try proof snippets without mutating source files.

ProofAttemptRow

Per-candidate proof attempt result row.

ProofBoundaryCandidate

Valid proof-state boundary a selector can target.

ProofCandidate

One proof candidate to splice into an in-memory overlay.

ProofPositionSummary

Informational summary of the resolved proof position.

ProofStateInfo

Proof-state payload for one cursor.

ReferencesResult

Result for ModuleQuery::References.

RenderedInfo

Bounded rendered Lean text.

Enums

DeclarationTargetResult

Result for ModuleQuerySelector::DeclarationTarget.

DeclarationVerificationBatchOutcome

Header-aware batch declaration-verification outcome.

DeclarationVerificationOutcome

Header-aware declaration verification outcome.

DeclarationVerificationStatus

Verification policy result.

DeclarationVerificationTarget

Target declaration for verification.

GoalAtResult

Result for ModuleQuery::GoalAt.

ModuleQuery

Query shape for one header-aware Lean module processing request.

ModuleQueryBatchCachedOutcome

Header-aware batched module-query outcome with cache/timing facts.

ModuleQueryBatchItem

One selector result in a batched module query.

ModuleQueryBatchOutcome

Header-aware batched module-query outcome.

ModuleQueryBatchResult

Typed payload returned by one successful batch selector.

ModuleQueryCacheStatus

Worker-side module snapshot cache status for a batched module query.

ModuleQueryOutcome

Header-aware module-query outcome.

ModuleQueryResult

Typed payload returned by a successful module query.

ModuleQuerySelector

One selector inside a batched module-processing request.

ProofAttemptOutcome

Header-aware proof attempt outcome.

ProofAttemptStatus

Per-candidate proof attempt status.

ProofEditTarget

Target for a non-mutating proof attempt.

ProofPositionSelector

Intent selector for one proof position inside a declaration.

ProofStateResult

Result for ModuleQuerySelector::ProofState.

SorryPolicy

Policy for sorry-like constructs during declaration verification.

SurroundingDeclarationResult

Result for ModuleQuerySelector::SurroundingDeclaration.

TypeAtResult

Result for ModuleQuery::TypeAt.