The Coq mailing list

["Roly Perera" <roly.perera AT dynamicaspects.org>]

2009/1/8 muad 
<muad.dib.space AT gmail.com>:

> Since Coqs positivity check will actually inspect the constructors of any
> inductives used in a constructor declaration (in this case fhlist), if you
> define fhlist as an inductive family instead of a function the definition of
> term is accepted.
> The fhmember and fhget functions are roughly the same but without proof
> irrelevance there are some times when writing functions over inductive
> families can be very difficult in comparison so I just include this code in
> case it is interesting.

Thanks for that extra info.  My version of Coq (8.1pl3) didn't seem to
like the curly brackets in the Fixpoint definitions; is there some
notation I have to enable?

> Fixpoint fmember {xs} (ls: fhlist xs): Type :=