## Stream: new members

### Topic: Inductive Types

#### Yasmine Sharoda (Oct 26 2020 at 19:47):

Hello, I am writing my first program in lean. I defined the following inductive type

inductive Expr (A : Type)
| singleton : A -> Expr


Expr is a parameterized type, and so instances would have type Expr A for some type A. But the occurrence of the type Expr in the definition of singleton does not include the parameter? Is their a good reason?
PS: I am type checking this using the online tool: https://leanprover.github.io/live/latest/

#### Mario Carneiro (Oct 26 2020 at 19:47):

It does actually have the parameter, as you can see with #print Expr.singleton

#### Mario Carneiro (Oct 26 2020 at 19:48):

but in the definition, the parameters to the inductive type are left off so you can't change them

#### Yury G. Kudryashov (Oct 26 2020 at 19:49):

You're not allowed to use Expr with any other parameter inside | singleton : A → Expr line, so you don't write the parameter at all.

#### Mario Carneiro (Oct 26 2020 at 19:50):

technically speaking, inside the types for the constructors, a local variable called Expr : Type is available for use to refer to the type being defined, and when the constructor is actually created, this variable is replaced with Expr A where Expr : Type -> Type is the new constant

Last updated: May 12 2021 at 04:19 UTC