Module nested 

Nested-to-mutual inductive elaboration (C10).

A nested inductive is one whose constructor fields mention the type being defined under an already-declared foreign container, e.g. node : Array Syntax → Syntax (Syntax occurs inside Array). Lean’s kernel compiles these by SPECIALIZING each container into an auxiliary mutual inductive (the family type becomes a fresh leading parameter), CHECKING that genuinely-mutual family with the ordinary machinery, then RESTORING recursors stated over the real container, which are what is installed and what an exported recursor is held against.

This module is built in stages (see docs/audit/2026-07-17-nested-inductives/design.md):

• S1 (this file, now): detect — recover the container C, its level arguments, its argument spine, and which argument positions mention a family-being-defined type. Behaviour of the kernel is unchanged; nested inductives are still rejected at the positivity leaf in derive.rs.
• S2: specialize — copy the container’s mutual block into fresh auxiliaries, abstracting the family-occurring args as new leading params.
• S3: restore — repackage the derived recursors over the real container and drop the abstracted parameters.

Structs

AuxMap

How one auxiliary inductive maps back to the real container it specializes. Retained through derivation so S3 restoration can substitute the auxiliary type / constructors / recursor back to the real container constants and drop the abstracted parameters.

ExpandedFamily

The nesting-free mutual family produced by specialize: the originals (with nested container applications rewritten to auxiliary references) followed by the freshly-synthesized auxiliary inductives.

NestedOcc

A nested occurrence C Ds Is: a family-being-defined type appears inside the arguments of an already-declared foreign inductive C.

Functions

check_and_derive_family_nested

Nested-aware family derivation. When specs contains a nested inductive, specialize it into an auxiliary mutual family and derive that (returning the ExpandedFamily so S3 can restore the recursors); otherwise fall back to the ordinary check_and_derive_family.

detect

Detect a nested occurrence at a strict-positivity leaf.

restore

Restore a raw expanded-family derivation (S3): rewrite the auxiliary type-formers / constructors back to the real container in every recursor type and rule, re-key rules by the real constructor, drop the auxiliary inductives and constructors, keep only the original types’ inductives and constructors (with num_nested set and all narrowed to the originals), and RETAIN the auxiliary recursors — now stated over the real container — because reducing a user-facing recursor still emits them.

specialize

Specialize the nested container occurrences of specs into an auxiliary mutual family (S2). Returns Ok(None) when there is no nesting (the caller should use the ordinary derivation path), or when the shape is not yet supported by this stage (parametrized families or multi-member containers), in which case the ordinary path re-produces the current UnsupportedNested verdict — so behaviour never silently changes.

verify_nested_bundle

Verify a nested inductive bundle for export replay and return the kernel-derived family to install (recursors renamed to the exported names and put under the exported universe parameter names).