Function derive_native_recursors_with_params 

pub fn derive_native_recursors_with_params(
    ctx: &Context,
    decl: &NestedDecl,
    num_params: usize,
) -> KernelResult<Vec<NativeRecursor>>

derive_native_recursors for a nested inductive with num_params uniform parameters. The restored recursors abstract the parameters first, exactly as Lean’s generated nested recursors do (PTree.rec : {α : Type} → {motive_1 …} → {motive_2 …} → …).