The Coq mailing list

[roconnor AT theorem.ca]

On Thu, 29 Jun 2006, Line Jakubiec-Jamet wrote:

>  Hello,
>
> I have two questions about coercions in Coq.
>
> * 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: *)

Coercions are between classes, rather than types.  A class is a defined 
name with type forall (x1:A1)..(xn:An), s whre s is a sort, or Sortclass 
or Funclass.

If you define AB := {A}+{B} and AC := {A}+{C}, then you can make a 
coercion from AB to AC.

--
Russell O'Connor                                      <http://r6.ca/>
``All talk about `theft,''' the general counsel of the American Graphophone
Company wrote, ``is the merest claptrap, for there exists no property in
ideas musical, literary or artistic, except as defined by statute.''