Crate rlean_search 

rlean-search: type-aware search over Lean 4 theorems, lemmas, and axioms.

Schema namespace: http://github.com/createyourpersonalaccount/rlean-search

Re-exports

pub use ast::DeclKind;

pub use ast::Declaration;

pub use ast::IndexDocument;

pub use ast::TypeExpr;

pub use ast::RLEAN_NS;

pub use index::build_index;

pub use index::SearchIndex;

pub use search::matches_decl;

pub use search::matches_type;

pub use search::SearchHit;

Modules

ast

Abstract syntax for Lean 4 types and declarations.

cache

On-disk gzipped XML cache for one-shot invocations (index.xml.gz).

daemon

Tokio multi-client daemon serving JSONL / XML type search.

index

In-memory inverted index for fast type search.

lake

Lake build system / package manager hierarchy awareness.

lexer

Lexer for a useful fragment of Lean 4 type / declaration surface syntax.

parser

Parsers for Lean type expressions and theorem/lemma/axiom declarations.

protocol

JSONL and XML request/response protocol for the daemon and client.

search

Fast type-aware pattern matching with holes and named holes.

xml

XML serialization / deserialization for the rlean-search schema.