The Coq mailing list

[Daniel Schepler <dschepler AT gmail.com>]

On Tue, Sep 16, 2014 at 2:11 AM, Cedric Auger 
<sedrikov AT gmail.com>
 wrote:
> Yes, that is clever.
> By the way, I do not know why people use this definition of "fin" which I
> find rather inconvenient.
>
> Inductive emptySet : Type := .
>
> Fixpoint fin2 (n : nat) : Type := match n with O => emptySet | S n => option
> (fin2 n) end.
>
> is a lot more convenient from my point of view.
> Here, we do not have to do all these inversion stuff when inspecting an
> element.

I've often found that inductive versions have nicer extractions to
OCaml than the corresponding Fixpoint to Type or Set definitions whose
extractions require a lot of Obj.magic.
-- 
Daniel Schepler