The Coq mailing list

[Siddharth Bhat <siddu.druid AT gmail.com>]

Thank you, that does help.

How does the set notation work? I haven't seen that before, that is cool.

Is there some place that uses Fin in some trivial way? Eg. Establishes a bijection with [1..n]? If not, I suppose I can stumble through :)

Thanks
Siddharth

On Wed 10 Jan, 2018, 11:36 ikdc, <ikdc AT mit.edu> wrote:

On 01/10/2018 12:58 AM, Siddharth Bhat wrote:
> Hello all, I'm looking for a type that encodes the fact that its
> inhabitants are naturals from 1 to N.
>
> I believe Fin is the type I am looking for? I'm not sure what Fin
> represents, exactly. Does Fin act as a witness for the *entire interval*
> [1..n]? Or can it witness some k \in [1..n]?
>
> Ideally. There would be a type (forall n : nat), "T n" whose inhabitants
> can be put in bijection with [1..n]
>
> Thanks
> Siddharth
>

Fin N is indeed such a type.  The two constructors represent the following:
- Fin (N + 1) has one element for each element of Fin N
- as well as one extra element

Hopefully that explains its definition.

I believe it is isomorphic to the type { n : nat | n < N } (or
alternatively { n : nat | 0 < n /\ n <= N }) which may be easier to work
with depending on what you're trying to do.

ikdc

--

Sending this from my phone, please excuse any typos!