• The checker is defined in terms of reduction to plain inductives, although the reduction itself is not performed before going to the kernel (it was in lean 3 but this lead to performance issues).
• The recursor for the type is basically "whatever the analogous mutual inductive would have".

inductive Const : Type _ | mkinductive Const1 (t: Type _) : Type _ | mk : Const1 tinductive E : Const → Type| mk : {c : Const} → (args : Const1 (E c)) → E Const.mk-- (kernel) invalid nested inductive datatype 'Const1',-- nested inductive datatypes parameters cannot contain local variables.