lean-rs-host 0.3.1

Opinionated Rust host stack for embedding Lean 4 as a theorem-prover capability: typed sessions, kernel-check evidence handles, bounded MetaM services, progress, batching, and session pooling.
Documentation 
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23

//! 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.

mod query;

pub use self::query::{
    DeclarationOutlineResult, DeclarationTargetInfo, DeclarationTargetResult, DeclarationVerificationBatchItem,
    DeclarationVerificationBatchOutcome, DeclarationVerificationBatchRequest, DeclarationVerificationBatchRow,
    DeclarationVerificationFacts, DeclarationVerificationOutcome, DeclarationVerificationRequest,
    DeclarationVerificationStatus, DeclarationVerificationTarget, GoalAtResult, LocalInfo, ModuleQuery,
    ModuleQueryBatchCachedOutcome, ModuleQueryBatchEnvelope, ModuleQueryBatchItem, ModuleQueryBatchOutcome,
    ModuleQueryBatchResult, ModuleQueryCacheFacts, ModuleQueryCachePolicy, ModuleQueryCacheStatus, ModuleQueryOutcome,
    ModuleQueryOutputBudgets, ModuleQueryResult, ModuleQuerySelector, ModuleQueryTimings,
    ModuleSnapshotCacheClearResult, ModuleSourceSpan, NameRefNode, ProofAttemptEnvelope, ProofAttemptOutcome,
    ProofAttemptRequest, ProofAttemptRow, ProofAttemptStatus, ProofBoundaryCandidate, ProofCandidate, ProofEditTarget,
    ProofPositionSelector, ProofPositionSummary, ProofStateInfo, ProofStateResult, ReferencesResult, RenderedInfo,
    SorryPolicy, SurroundingDeclarationResult, TypeAtResult,
};