How to create element of type `fin 0`

Stream: new members

[Rui Liu]

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]

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

[Yakov Pechersky]

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

[Bryan Gin-ge Chen]

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]

I guess docs#fin.elim0 is the same.

[Rui Liu]

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]

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

[Rui Liu]

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

[Bryan Gin-ge Chen]

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]

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