14.6 Declaration of Coercions

14.6.1 Coercion qualid : class1 >-> class2.

Declares the construction denoted by qualid as a coercion between class1 and class2.


Error messages:
  1. qualid not declared
  2. qualid is already a coercion
  3. FUNCLASS cannot be a source class
  4. SORTCLASS cannot be a source class
  5. Does not correspond to a coercion
    qualid is not a function.
  6. Cannot find the source class
  7. qualid does not respect the inheritance uniform condition
  8. The target class does not correspond to class2
When the coercion qualid is added to the inheritance graph, non valid coercion paths are ignored; they are signaled by a warning.
Warning :
  1. Ambiguous paths: [f11;..;fn11] : C1>->D1
    ...
    [f1m;..;fnmm] : Cm>->Dm

Variants:
  1. Coercion Local qualid : class1 >-> class2.
    Declares the construction denoted by qualid as a coercion local to the current section.

  2. Coercion ident := term
    This defines ident just like Definition ident := term, and then declares ident as a coercion between it source and its target.

  3. Coercion ident := term : type
    This defines ident just like Definition ident : type := term, and then declares ident as a coercion between it source and its target.

  4. Coercion Local ident := term
    This defines ident just like Local ident := term, and then declares ident as a coercion between it source and its target.

14.6.2 Identity Coercion ident:class1 >-> class2.

We check that class1 is a constant with a value of the form [x1:T1]..[xn:Tn](class2 t1..tm) where m is the number of parameters of class2. Then we define an identity function with the type (x1:T1)..(xn:Tn)(y:(class1 x1..xn)) (class2 t1..tm), and we declare it as an identity coercion between class1 and class2.


Error messages:
  1. Clash with previous constant ident
  2. class1 must be a transparent constant

Variants:
  1. Identity Coercion Local ident:ident1 >-> ident2.
    Idem but locally to the current section.