The Coq mailing list

[Andrej Bauer <andrej.bauer AT andrej.com>]

> Inductive endpoints (T : Type) : nat -> Type :=
> | End : T -> endpoints T O
> | Step : forall n (a b : endpoints T n), a = b -> endpoints T (S n).
>
> I don't know if it is what you wish.
> Typically, if you have something of type "endpoints T 2", you can
> decompose it into:
> a : T
> b : T
> c : T
> d : T
> Hab : End a = End b (* thus a = b *)
> Hcd : End c = End d (* thus c = d *)
> Habcd : Step Hab = Step Hcd

Thanks. I would have to think a bit about this because we get the
unwanted wrappers "Step (Step ... End a)...)". This may complicate
matters a bit. For a perfect solution we'd also want a function which
strips off the "End"s and "Steps" so that, for example, Hab above
would have the type a = b and Habcd woudl have the type Hab = Hcd.

But it is perhaps easier to use your definition and define an
auxiliary function which performes the stripping as an afterthought.

With kind regards,

Andrej