The Coq mailing list

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

> Fixpoint endpoints (n : nat) (X : Type) : Type :=
>  match n return Type with
>    | 0 => unit
>    | S n => {e : endpoints n X & path n X e & path n X e}
>  end
> with path (n : nat) (X : Type) (e : endpoints n X) : Type :=
>  match n return Type with
>    | 0 => X
>    | S n =>
>      match e with
>        | existT2 _ x y => x = y
>      end
>  end.
>
> but Coq doesn't like "endpoints" showing up in the type signature of
> path. Hope this helps.

Thanks! This is precisely the sort of thing I need. How do I make Coq happy?

With kind regards,

Andrej