The Coq mailing list

[Venanzio Capretta <venanzio AT site.uottawa.ca>]

On Fri, 2005-07-10 at 09:38 +0200, 
vincent.chatel AT transport.alstom.com
wrote:
> Thanks, but in this case I cannot construct a poly_list of poly_list.
> 
> And when I assume that X : Type, I have a Universe Inconsistency
> 

You need impredicativity for both these things. If you launch coq with
the -impredicative-set option (for example "coqide -impredicative-set"),
then you can do this:

--------------------------------------------------------------------
Inductive poly_list: Set :=
  poly_nil: poly_list
| poly_cons: forall X:Set, X -> poly_list -> poly_list.

Implicit Arguments poly_cons [X].

Definition pl:=(poly_cons true (poly_cons 3 poly_nil)).

Check (poly_cons pl pl).
---------------------------------------------------------------------

Cheers,
  Venanzio