2.7 Implicit Coercions

Coercions can be used to implicitly inject terms from one ``class'' in which they reside into another one. A class is either a sort (denoted by the keyword SORTCLASS), a product type (denoted by the keyword FUNCLASS) or an inductive type (denoted by its name).

Then the user is able to apply an object that is not a function, but can be coerced to a function, and more generally to consider that a term of type A is of type B provided that there is a declared coercion between A and B.

2.7.1 Class ident.

Declares the name ident as a new class.


Variant:
  1. Class Local ident.
    Declares the name ident as a new local class to the current section.

2.7.2 Coercion ident : ident1 >-> ident2.

Declares the name ident as a coercion between ident1 and ident2. The classes ident1 and ident2 are first declared if necessary.


Variants:
  1. Coercion Local ident : ident1 >-> ident2.
    Declares the name ident as a coercion local to the current section.

  2. Identity Coercion ident:ident1 >-> ident2.
    Coerce an inductive type to a subtype of it.

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

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

  5. 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.

  6. 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.

2.7.3 Displaying available coercions

Print Classes.

Print the list of declared classes in the current context.

Print Coercions.

Print the list of declared coercions in the current context.

Print Graph.

Print the list of valid path coercions in the current context.
See also: the technical chapter 14 on coercions.