Twelve ways to build
a Lean expression.
What the kernel sees is not a paragraph of tactics. It is a typed expression built from twelve constructor forms. Here is the complete structural alphabet our CoreGIR exporter handles, each with an explicit visual interface, a Lean example, and its limits.
Three different languages must not be confused
Lean source
theorem, def, by, pattern matching, tactics, notation and macros. Rich, expandable syntax.
Core expression
Applications, binders, constants, projections, literals, metadata and references. Twelve constructors, formal scope.
Kernel
Checks a term has its expected type in an environment. Drawings are explanatory views, not substitutes for checking.
Every node has a rule.
Select a form to explore its inputs, output, binding behavior and examples. The coloring indicates abstract syntax roles—not theorem truth values. Six forms were observed in the exported SE(2) benchmark; the other six are part of the universal exporter.
Loading the Lean expression visual grammar…
What this does—and doesn't—claim
These diagrams provide a proposed visual grammar for the complete Lean.Expr constructor algebra. They do not yet constitute a certified translation of the entire Lean surface grammar, a tactic-language visualizer, or a proof-net calculus for every theorem. Terms still need typed boundaries, references and environments; scope cannot be inferred from mere visual proximity.
The initial research benchmark is a public anonymized structural projection of CrossingData.crossing. The Lean.Expr reference and our exhaustive CoreGIR exporter define the scope of the twelve rules.