Zulip Chat Archive

Stream: general

Topic: Reference Manual


view this post on Zulip Yasuaki MORITA (Jul 02 2019 at 20:27):

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.

view this post on Zulip Mario Carneiro (Jul 02 2019 at 20:34):

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

view this post on Zulip Mario Carneiro (Jul 02 2019 at 20:34):

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

view this post on Zulip Mario Carneiro (Jul 02 2019 at 20:35):

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

view this post on Zulip Mario Carneiro (Jul 02 2019 at 20:37):

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

view this post on Zulip Yasuaki MORITA (Jul 02 2019 at 20:39):

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!


Last updated: May 13 2021 at 06:15 UTC