poka.sh

 Docs

LEAN

Generated by scripts/gen-format-pages.py from docs/data/format-metadata/, FILE_FORMATS.csv and docs/formats-master.csv. Do not edit by hand: change the source, then run the script.

Lean Preview.

At a glance
Purpose Lean source code (Lean 4 or Lean 3): definitions, theorems and proofs for the Lean prover.
Extensions .lean
Poka parser poka-lean
Viewer poka-metadata-card-viewer
Depth tier Metadata card (see Depth tiers)
Breadth tier B4 Summary (see Breadth tiers)

How much Poka reads

B4 Summary. The container and metadata are read and summarised (counts, properties, structure), but the main content is not rendered.

Confidence: medium (the reviewer read the code). Basis: Reviewed 2026-10-26: read parsers/poka-lean/src/main.rs (342 lines) and plugin.json in full. The crate has no unit tests and no tests/samples.rs, and the corpus has no .lean sample, so the tier rests on reading the code. Covers .lean. The output is a metadata card of counts found by matching text line by line: imports, namespaces, sections, theorems and lemmas, definitions, examples, inductives, structures, classes and instances, macros, abbrev and notations, variable and universe declarations, by blocks and tactic calls, sorry occurrences and line counts. Judgement: B4, because the structure is summarised but the source itself is never shown.

What Poka does not read

  • The source text is not shown: the card carries only counts and a few sample names, with no code view or highlighting
  • Constructs are found by matching text line by line, not by parsing, so multi-line declarations, nested or indented definitions and keywords inside strings or comments can be miscounted
  • Counts of named items stop where their name list is capped (imports at 64), so a larger file under-reports them
  • Files over 64 MiB are cut to the first 64 MiB (the card says so)
  • Text that is not UTF-8 is decoded with replacement characters; no other encoding is tried
  • Lean 3 and Lean 4 are not told apart

Libraries

Libraries Poka uses or has assessed for this format, with the status, licence and language the registry records.

  • tree-sitter-lean (candidate; MIT; JavaScript/C (tree-sitter); https://github.com/Julian/tree-sitter-lean) — Experimental tree-sitter grammar for Lean 4; editor-tooling parser, not a faithful reproduction of Lean's own parser.

Sources

  • parsers/poka-lean/src/main.rs
  • parsers/poka-lean/plugin.json