Module printer 

The kernel’s surface, written back: the exact inverse of term_parser and command_parser.

For every term and command the printer spells, parsing the text in a fresh context yields the same term (up to α) — vernacular_roundtrip.rs locks that. A term with no surface spelling is a PrintError, never an approximation: the caller reports source export as unsupported.

What “the same term” means

The text is read back exactly as the Repl reads it: the term door, then name resolution at the root scope against the environment the term lives in. That second stage is where a qualified reference Nat.add becomes the constant Nat.add rather than the field add of Nat — LOGOS’s own staging, the one Lean has — so the printer writes qualified names as qualified names rather than escaping them.

Binders

A kernel term names its binders, and a name that does not read back BARE as that binder is RENAMED rather than printed as is — α-renaming changes nothing the kernel can see. A binder is renamed when its name would capture a global the body mentions (a binder x over a body naming the global x, or a binder Nat over a body naming Nat.add), when the plain grammar reads it as something else (a keyword, a sort, _ that is referred to), or when it could be written only in guillemets (the importer’s arena.local.3) — a quoted binder name tells a reader nothing. A fresh name is fresh against EVERY name the term spells, so a renamed binder can neither capture nor be captured. Every other binder keeps its name. Globals are never renamed: a constant is spelled bare, qualified, or «quoted», and always means itself.

Depth

Imported terms are deep. Both passes here — the scan that learns which binders are referred to, and the printing itself — run on an explicit work stack, so printing a term never recurses once per level of it.

Enums

PrintError

A term or command the LOGOS surface cannot spell (yet).

Functions

inductive_command

The vernacular command that registers the inductive block name belongs to, EXACTLY as ctx holds it — its universe telescope, each member’s written parameters (the context’s declared parameter count), its arity past them, and each constructor’s type past them.

print_command

Spell command as one vernacular command, terminated by its period.

print_term

Spell term in the kernel term surface.

print_term_in

Spell term read in a context whose locals are locals: each prints as its own name. A goal and its hypotheses are spelled this way for a reader; a closed term’s round trip is print_term’s, which refuses a free name because the surface would read it as a global.

structure_commands

The commands that make name a STRUCTURE exactly as ctx holds it: each projection’s definition (under the inductive’s universe telescope), then Structure name := proj₀ … projₙ. Empty when ctx holds no structure information for name. Emit them right after the block from inductive_command, before anything — a recursor whose body is written through the projections, say — relies on structure η.