## Stream: new members

### Topic: How to create element of type fin 0

#### Rui Liu (Dec 07 2020 at 21:53):

I feel there should be an easy way to create element of type fin 0, since there's only one such function. How to do it?

#### Yakov Pechersky (Dec 07 2020 at 21:54):

In fact, there are zero such terms, so it is impossible to construct such an "element".

#### Yakov Pechersky (Dec 07 2020 at 21:54):

If you somehow did have an i : fin 0, then that can be used to produce a proof of false.

#### Bryan Gin-ge Chen (Dec 07 2020 at 21:55):

As Yakov explains, fin 0 is an empty type, but the unique function out of it is docs#fin_zero_elim.

#### Bryan Gin-ge Chen (Dec 07 2020 at 21:58):

I guess docs#fin.elim0 is the same.

#### Rui Liu (Dec 07 2020 at 21:58):

Oh no, I was trying to use fin n -> T in my inductively defined type, since I cannot use vector T n in an inductive definition as it violates positivity constraints.

How would I do it in inductive type then?

#### Kevin Buzzard (Dec 07 2020 at 21:59):

There's a function fin 0 -> T. What are you worried about?

#### Rui Liu (Dec 07 2020 at 22:03):

Oh right, I guess although fin 0 cannot be constructed, fin 0 -> T can be constructed? @Kevin Buzzard

#### Bryan Gin-ge Chen (Dec 07 2020 at 22:07):

variables (T : Type*)
#check (@fin.elim0 (λ _, T) : fin 0 → T)


I think in most cases you should be able to use fin.elim0 or fin_zero_elim without making the function type explicit.

#### Eric Wieser (Dec 07 2020 at 22:14):

Note that if T is not empty, you can use the simpler (λ _ : fin 0, some_t)

Last updated: Dec 20 2023 at 11:08 UTC