Reference Manual

Stream: general

[Yasuaki MORITA]

I saw The Lean Reference Manual and I found a description of inductive type declaration which I could not understand.

https://leanprover.github.io/reference/declarations.html#inductive-types

This is a quote from 4.4 Inductive Types in the document.

Suppose the telescope (b : βᵢ) is (b₁ : βᵢ₁) ... (bᵤ : βᵢᵤ). Each argument in the telescope is either nonrecursive or recursive.

An argument (bⱼ : βᵢⱼ) is nonrecursive if βᵢⱼ does not refer to foo, the inductive type being defined. In that case, βᵢⱼ can be any type, so long as it does not refer to any nonrecursive arguments.
An argument (bⱼ : βᵢⱼ) is recursive if it βᵢⱼ of the form Π (d : δ), foo where (d : δ) is a telescope which does not refer to foo or any nonrecursive arguments.

This description says that each argument in the telescope is either nonrecursive or recursive.
I can not get from the following statements even whether or not nonrecursive and recursive arguments are mutually exclusive.
My intuition tells recursive argument means that it refer to foo itself in some sense.
But these statements seem to say that none of the arguments refer to foo.

[Mario Carneiro]

nonrecursive and recursive are mutually exclusive and exhaustive of the arguments to a constructor

[Mario Carneiro]

Recursive means it has the form Π (d : δ), foo, so it clearly refers to foo and hence it cannot be nonrecursive

[Mario Carneiro]

If an argument fits neither description (neither nonrecursive nor recursive), for example foo -> foo, then it is not allowed as a constructor argument at all

[Mario Carneiro]

The rule says that (d : δ) is a telescope that does not refer to foo, so the only appearance of foo in Π (d : δ), foo is the one at the end

[Yasuaki MORITA]

so the only appearance of foo in Π (d : δ), foo is the one at the end

Oh, I have missed foo in Π (d : δ), foo . I understood. Thank you!