pub fn inductive_command(
ctx: &Context,
name: &str,
) -> Result<Command, PrintError>Expand description
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.
★ THE PARAMETER SPLIT IS THE SUBTLE PART, SO IT IS WRITTEN ONCE, HERE. The command surface
refers to a parameter, inside the arity and the constructor types, as the GLOBAL of its name —
the registration then binds every global of that spelling. So a parameter must be named by a
spelling nothing else in those terms uses: not a constant they mention (it would be captured
and bound), and not a binder inside them (the conversion would reach under it and be captured
in turn). The kernel’s own binder name is kept when it is safe, which keeps Lean’s α, and a
fresh one is chosen otherwise.
The command is built, not printed: pass it to print_command for the text.