Zulip Chat Archive

Stream: new members

Topic: Question regarding Inductive Types

Rajiv (Dec 03 2020 at 11:57):


I am new to Lean and I am trying to understand Inductive Types in Lean. Specifically, in section 4.4 of Lean Reference Manual (https://leanprover.github.io/reference/declarations.html#inductive-types), following is mentioned.

The declaration of the type foo as above results in the addition of the following constants to the environment:

the type former foo : Π (a : α), Sort u

for each i, the constructor foo.constructorᵢ : Π (a : α) (b : βᵢ), foo a

In case I have a simple inductive type definition such as

inductive ty_former : Type
| test_con : ty_former

What values would (a : α) take?

Would I be right in understanding that the constants generated would be something of the form

ty_former : Π (a : α), Type 0

test_con : Π (a : α), ty_former a

Marc Huisinga (Dec 03 2020 at 12:11):

a : α are the "fixed" parameters of the inductive type, as described at the top of the section 4.4. in your example, there are no such parameters.

Rajiv (Dec 03 2020 at 12:20):

Thanks Marc. My apologies. I could not find where "fixed" parameters is described.

Is it the case that in the form,

inductive foo (a : α) : Sort u
| constructor₁ : Π (b : β₁), foo
| constructor₂ : Π (b : β₂), foo
| constructorₙ : Π (b : βₙ), foo

(a : α) and Π (b : β₁) are optional?

Marc Huisinga (Dec 03 2020 at 12:29):

in this case, (a : α) and (b : β₁) do not refer to single type annotations, but telescopes (i.e. a sequence of type annotations), like in section 4.2. the sequence can be empty.

Rajiv (Dec 03 2020 at 13:27):

Thanks Marc.

Last updated: Dec 20 2023 at 11:08 UTC