Question regarding Inductive Types

Stream: new members

[Rajiv]

Hi,

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]

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]

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]

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]

Thanks Marc.