pub fn structure_commands(
ctx: &Context,
name: &str,
) -> Result<Vec<Command>, PrintError>Expand description
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 η.