The Coq mailing list

[Claudio Sacerdoti Coen <sacerdot AT cs.unibo.it>]

> I really want to define
> 
> Inductive Lambda : Set -> Set :=
>  | var : forall A:Set, A -> Lambda A
>  | app : forall A:Set, Lambda A -> Lambda A -> Lambda A
>  | lambda : forall A:Set, Lambda (option A) -> Lambda A.
> 
> which is almost uniformly parametric polymorpic.  This definition strikes
> me as just as safe as polymorphic lists.
> 
> I cannot fix this my changing Set to Type because then the statement of
> the join function:
> 
> Definition joinStatement :=
>    forall (T:Type)(l:Lambda (Lambda T)),(Lambda T).
> 
> causes a universe inconsistency.

 The inductive definition Lambda you give above obtained replacing Set with
 Type and the joinStatement above does not cause a universe inconsistency.
 The universe inconsistency must be generated by something else you are
 doing, and it may be possible to avoid it.

                                        Regards,
                                        C.S.C.

-- 
----------------------------------------------------------------
Real name: Claudio Sacerdoti Coen
Doctor in Computer Science, University of Bologna
E-mail: 
sacerdot AT cs.unibo.it
http://www.cs.unibo.it/~sacerdot
----------------------------------------------------------------