Zulip Chat Archive

Stream: new members

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


view this post on Zulip 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?

view this post on Zulip Yakov Pechersky (Dec 07 2020 at 21:54):

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

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip Bryan Gin-ge Chen (Dec 07 2020 at 21:58):

I guess docs#fin.elim0 is the same.

view this post on Zulip 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?

view this post on Zulip Kevin Buzzard (Dec 07 2020 at 21:59):

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

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip 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: May 13 2021 at 06:15 UTC