Function compile_nested_with_params 

pub fn compile_nested_with_params(
    ctx: &Context,
    decl: &NestedDecl,
    num_params: usize,
) -> KernelResult<Compiled>

compile_nested for an inductive with num_params uniform parameters (PTree α := node : α → List (PTree α) → PTree α).

The parameters are split off the sort and every constructor onto one canonical telescope (see Nesting). The base leaf of specialization is the inductive at exactly those parameters; every specialized sibling takes the same telescope as its uniform parameters (PTree$List α), and every conversion iso abstracts it. An occurrence of the inductive at any other arguments is a non-uniform nesting and is refused, as are constructor results that do not return the inductive at its own parameters.