The Coq mailing list

[Paolo Herms <paolo.herms AT cea.fr>]

On Thursday 21 July 2011 14:25:59 AUGER Cedric wrote:
> I guess the problem is that you define a coercion from C' to C;
> and you would like to have one from C to C';
> so that you can branch it to follow this diagram: C>->C'>->D.
> 
> But I guess, that such a coercion is not possible.
> 
Identity Coercions are supposed to work in both directions, that's why
Check c : C' X Y.
works.

> I don't know if you are interested in this:
> 
> Parameter C : Type -> Type.
> Parameter D : Type -> Type -> Type.
> Parameter f : forall A, C A -> forall B, D A B.
> 
> Coercion f: C>-> Funclass.
> 
> Variable X: C nat.
> Check (X nat: D nat nat).
> Check (X: forall B, D nat B). 

No, at the points, where I want the coercion to work, the expected type is 
D ? ?.
-- 
Paolo Herms
PhD Student - CEA Software Safety Lab. / INRIA ProVal Project
Paris, France