The Coq mailing list

[Chris Casinghino <chris.casinghino AT gmail.com>]

Hello Yves,

> You should look at the pattern-matching constructs (for instance the value
> of hlist_rect), the fact that the parameter does not occur among the
> constructors' arguments plays a role.

I am confused.  Before sending my initial email, I observed that
hlist_rect doesn't change if I make A an index and an argument to each
constructor.  That is, this alternate version of hlist is given
an identical hlist_rect (up to alpha-conversion):

Inductive hlist : Type -> Type :=
 | HNil  : forall A : Type, hlist A
 | HCons : forall A : Type, forall B, A -> hlist B -> hlist A.

This was the source of my confusion, since I thought the point of
parameters was to get the nicer hlist_rect, as you suggest.  Am I
missing something?

> The only example using this feature that I know of is in a paper by
> Ralph Matthes.

Thank you for this reference and for the quick response.  I will have
a look

--Chris