Module lean 

The Lean 4 frontend for the portable core.

It reads the layout-sensitive subset that the core can represent faithfully: namespaces, inductive types, definitions (including equation-compiler style), match, if, let, theorems with their tactic structure, and a main : IO Unit of IO.println effects. Everything else is rejected with a precise obligation.

Mirrors js/src/translation/lean.js.

Functions

annotate_layout

Fills in each token’s line, column and whether it starts its line.

parse_lean

Reads a Lean program.

span

The range from from up to the start of to (the end of input adds nothing).