Module inductive_compile 

Nested-inductive compiler (K3) — the UNTRUSTED front-end for inductives that recur nested inside a container, RTree := rnode : TList RTree → RTree.

Such a type is not directly a strict-positivity-checkable inductive: RTree appears as an ARGUMENT of TList, not to the right of an arrow. The Lean/Coq resolution is SPECIALIZATION: replace the container TList RTree by a fresh sibling RTree$TList defined MUTUALLY with RTree, mirroring TList’s constructors with the element type fixed to RTree:

RTree       := rnode : RTree$TList → RTree
RTree$TList := RTree$TList_TNil | RTree$TList_TCons : RTree → RTree$TList → RTree$TList

This block is an ordinary mutual inductive (K3b), so its recursor recurses through the specialized list — the whole point. To relate the specialized form back to the generic TList RTree, the compiler emits CONVERSION ISOS RTree$TList ↔ TList RTree.

Crucially this module is UNTRUSTED: it only produces terms. The caller registers the mutual block through the trusted mutual machinery and TYPE-CHECKS every iso through the trusted kernel — a mis-compiled sibling or iso is rejected, never trusted. Zero new trusted code, exactly as Lean compiles nested inductives to mutual ones.

Structs

Compiled

The compiled artifacts of a nested inductive: the mutual block to register, and the iso DEFINITIONS (name, type, body) to kernel-check and add. Nothing here is trusted until the caller checks it.

IsoNames

One container specialized for this inductive, with the names of its conversion isos.

NestedDecl

A nested inductive declaration: a name, its sort, and constructors whose argument types may mention the inductive nested inside a registered container (TList RTree).

NestedInfo

What a nested-inductive registration produced: the specialized sibling type names and the conversion isos relating each to its generic container.

Functions

compile_nested

Compile a nested inductive into a mutual block plus conversion isos. Untrusted: every artifact is checked by the caller. Handles arbitrary nesting DEPTH (TList (TList RTree)) by recursive specialization — each container level becomes its own mutual sibling.