Incomplete requirements for nested inductive types

The section on Nested Inductive Types, and in particular, the list of requirements nested recursive occurrences must satisfy, is incomplete.

Nested recursive occurrences must satisfy the following requirements:

• They must be nested directly under an inductive type's type constructor. Terms that reduce to such nested occurrences are not accepted.
• Local variables such as the constructor's parameters may not occur in the arguments to the nested occurrence.
• The nested occurrences must occur strictly positively.

In what way is the content incorrect?

The list of requirements misses on two known requirements that must be satisfied in order for a nested inductive type to be correctly translated.

• A nested occurrence may not be used inside the rest of the constructor in a way that would have it rely explicitly on the type it's nested in, as that could lead to the construction of an inductive-recursive type. e.g

def Option.IsNone : Option α → Type := Option.rec Unit (fun _ => Empty)
inductive Foo where
  | foo : (l : Option Foo) → l.IsNone → Foo

Would need to be translated as the following inductive-recursive type to be well-formed:

mutual
  inductive Foo where
    | foo : OptionFoo → Foo
  inductive OptionFoo where
    | none
    | some : Foo → Option Foo
  def OptionFoo.IsNone : OptionFoo → Type
    | none => Unit
    | some _ => Empty
end

Instead, lean tries the naive mutual translation, and errors out when checking the translated constructors.

• A nested recursive occurrence may not appear in a parameter position that an index of the inductive type it's nested in may depend on. This one is further documented at lean4#6371, and also fails during translation instead of giving a good early error.

Furthermore, it should probably be noted that, in order for the translation to give rise to a strictly positive type, it is not only necessary that the nested recursive occurrence appear strictly positively inside another inductive type's type constructor (as pointed out in the list of requirements), but also that the type constructors the nested occurrences appear in appear themselves in a strictly positive manner. e.g in the following code, the recursive occurrence Foo appears strictly positively in Option Foo, but Option Foo itself does not appear strictly positively in the constructor, and is thus not accepted.

inductive Foo where
  | foo : (Option Foo → Nat) → Foo

Lastly, this is more of a suggestion, but Lean, might benefit from making explicit the exact positivity criteria(s) the system allows for, similarly to Rocq's presentation on the matter.

Start with the Nested Inductive Types section linked in the issue and review the existing list of requirements alongside the examples provided. Check lean4#6371 for the additional parameter-position constraint. Done means the documentation covers the two missing restrictions and the broader strict-positivity condition, with the exact accepted criteria made explicit where possible.