Module parser 

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

Structs

SearchPattern

A user search pattern, optionally restricted to the conclusion (|-).

Functions

parse_declarations

Parse all theorem/lemma/axiom declarations from a .lean source string.

parse_declarations_with_path

parse_search_pattern

parse_type