The Coq mailing list

[Virgile Prevosto <virgile.prevosto AT m4x.org>]

Hello,

Le Thu, 29 Jun 2006 17:18:54 +0200,
Line Jakubiec-Jamet 
<jakubiec AT lif.univ-mrs.fr>
 a écrit :

> * My first problem is illustrated by the following declarations:
> 
> Parameters (A B C :Prop).
> Parameter Z:{A}+{B}->{A}+{C}.
> Coercion  Z:{A}+{B}>->{A}+{C}. (*Syntax error: *)

as already said, coercions are between classes, not arbitrary types

> * Secondly, suppose we have :
> 
> Parameters (A B C :Prop).
> Definition X:={A}+{B}.
> Definition Y:={A}+{C}.
> Parameter Z:X->Y.
> Coercion  Z:X>->Y.
> 
> Parameter F:Y->Prop.
> Definition f := exists v:B, F (Z (right A v)).
> 
> Why we have to use Z in the definition f to make the conversion
> between an object of type X to an object of type Y ?

I guess this is a side-effect of the above: (right A v) has type
{A}+{B}, not X. If you use a type annotation, the coercion is correctly
inferred:
(* ... *)
Definition f := exists v:B, F ((right A v): X).
Print f.
f = exists v : B, F (right A v:X): Prop
-- 
E tutto per oggi, a la prossima volta.
Virgile