The Coq mailing list

[Lionel Elie Mamane <lionel AT mamane.lu>]

Hi,

I'm trying to write the second projection of this type:

Inductive T:Type := T_cons: (I:Type) (I->T) -> T.

Is it possible?

The first projection goes without any problem:

Definition TProj1 := [t:T] Cases t of (T_cons It f) => It end.

But the second one fails with "Error: Inference of annotation not yet
implemented in this case".

So I thought I would just annotate the expression:

Definition TProj2 := [t:T] <(TProj1 t)->T>Cases t of (T_cons It f) => f end.

But Coq says "The term f has type It->T while it is expected to have
type (TProj1 t)->T". Replacing (TProj1 t) by its delta/beta-reduction
doesn't help:

Definition TProj2 := [t:T] <Cases t of (T_cons It f)=>It end>Cases t of 
(T_cons It f) => f end.
answers "The term f has type It->T while it is expected to have type
Cases t of (T_cons It _) => It end"

I tried:

Definition TProj2 : (t:T)(TProj1 t)->T := [t:T] Cases t of (T_cons It
f) => f end.

too, but same error message.


Thank you for your help,

-- 
Lionel