pub fn derive_nested_block_recursors(
ctx: &Context,
block: &NestedBlock<'_>,
) -> KernelResult<Vec<NativeRecursor>>Expand description
Reconstruct Lean’s recursors for a nested block: the elimination’s mutual recursors, each
restored to the source families and container instances and checked again in ctx.
The source members must already be registered in ctx exactly as declared. Recursors come in
block order: the source members, then the auxiliary families in discovery order.