pub fn compile_nested(
ctx: &Context,
decl: &NestedDecl,
) -> KernelResult<Compiled>Expand description
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.