# Zulip Chat Archive

## 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

#### Alex Zhang (Jun 15 2021 at 09:12):

If I define `mynat`

as follows

```
inductive mynat : Type
| zero : mynat
| succ : mynat → mynat
example : mynat.zero ≠ mynat.succ mynat.zero :=
begin
intros h,
sorry
end
example : function.injective mynat.succ :=
begin
intros a b h,
sorry
end
```

Then do I have "mynat.zero ≠ mynat.succ mynat.zero" and "mynat.succ is injective" by the definition? If so, how can I prove them?

#### Mario Carneiro (Jun 15 2021 at 09:16):

`nat.no_confusion`

can be used to prove both of them

#### Mario Carneiro (Jun 15 2021 at 09:17):

the equation compiler knows about both of these lemmas though so you can get some slicker proofs using it

```
example : mynat.zero ≠ mynat.succ mynat.zero.
example : function.injective mynat.succ | _ _ rfl := rfl
```

#### Alex Zhang (Jun 16 2021 at 06:05):

Could you please explain the function of `nat.no_confusion`

?

#### Kevin Buzzard (Jun 16 2021 at 06:05):

https://xenaproject.wordpress.com/2018/03/24/no-confusion-over-no_confusion/

Last updated: Dec 20 2023 at 11:08 UTC