<commit_before>.. include:: ../replaces.rst

.. _implicitcoercions:

Implicit Coercions
====================

:Author: <NAME>

General Presentation
---------------------

This section describes the inheritance mechanism of |Coq|. In |Coq| with
inheritance, we are not interested in adding any expressive power to
our theory, but only convenience. Given a term, possibly not typable,
we are interested in the problem of determining if it can be well
typed modulo insertion of appropriate coercions. We allow to write:

 * :g:`f a` where :g:`f:(forall x:A,B)` and :g:`a:A'` when ``A'`` can
   be seen in some sense as a subtype of ``A``.
 * :g:`x:A` when ``A`` is not a type, but can be seen in
   a certain sense as a type: set, group, category etc.
 * :g:`f a` when ``f`` is not a function, but can be seen in a certain sense
   as a function: bijection, functor, any structure morphism etc.


Classes
-------

A class with `n` parameters is any defined name with a type
:g:`forall (x₁:A₁)..(xₙ:Aₙ),s` where ``s`` is a sort.  Thus a class with
parameters is considered as a single class and not as a family of
classes.  An object of a class ``C`` is any term of type :g:`C t₁ .. tₙ`.
In addition to these user-classes, we have two abstract classes:


  * ``Sortclass``, the class of sorts; its objects are the terms whose type is a
    sort (e.g. :g:`Prop` or :g:`Type`).
  * ``Funclass``, the class of functions; its objects are all the terms with a functional
    type, i.e. of form :g:`forall x:A,B`.

Formally, the syntax of a classes is defined as:

.. productionlist::
   class: qualid
        : | `Sortclass`
        : | `Funclass`


Coercions
---------

A name ``f`` can be declared as a coercion between a source user-class
``C`` with `n` parameters and a target class ``D`` if one of these
conditions holds:

 * ``D`` is a user-class, then the type of ``f`` must have the form
   :g:`forall (x₁:A₁)..(xₙ:Aₙ)(y:C x₁..xₙ), D u₁..uₘ` where `m`
   is the number of parameters of ``D``.
 * ``D`` is ``Funclass``, then the type of ``f`` must have the form
   :g:`forall (x₁:A₁)..(xₙ:Aₙ)(y:C x₁..xₙ)(x:A), B`.
 * ``D`` is ``Sortclass``, then the type of ``f`` must have the form
   :g:`forall (x₁:A₁)..(xₙ:Aₙ)(y:C x₁..xₙ), s` with ``s`` a sort.

We then write :g:`f : C >-> D`. The restriction on the type
of coercions is called *the uniform inheritance condition*.

.. note:: The abstract classe ``Sortclass`` can be used as a source class, but<commit_msg>Fix typo in Coercions chapter.<commit_after>.. include:: ../replaces.rst

.. _implicitcoercions:

Implicit Coercions
====================

:Author: <NAME>

General Presentation
---------------------

This section describes the inheritance mechanism of |Coq|. In |Coq| with
inheritance, we are not interested in adding any expressive power to
our theory, but only convenience. Given a term, possibly not typable,
we are interested in the problem of determining if it can be well
typed modulo insertion of appropriate coercions. We allow to write:

 * :g:`f a` where :g:`f:(forall x:A,B)` and :g:`a:A'` when ``A'`` can
   be seen in some sense as a subtype of ``A``.
 * :g:`x:A` when ``A`` is not a type, but can be seen in
   a certain sense as a type: set, group, category etc.
 * :g:`f a` when ``f`` is not a function, but can be seen in a certain sense
   as a function: bijection, functor, any structure morphism etc.


Classes
-------

A class with `n` parameters is any defined name with a type
:g:`forall (x₁:A₁)..(xₙ:Aₙ),s` where ``s`` is a sort.  Thus a class with
parameters is considered as a single class and not as a family of
classes.  An object of a class ``C`` is any term of type :g:`C t₁ .. tₙ`.
In addition to these user-classes, we have two abstract classes:


  * ``Sortclass``, the class of sorts; its objects are the terms whose type is a
    sort (e.g. :g:`Prop` or :g:`Type`).
  * ``Funclass``, the class of functions; its objects are all the terms with a functional
    type, i.e. of form :g:`forall x:A,B`.

Formally, the syntax of a classes is defined as:

.. productionlist::
   class: qualid
        : | `Sortclass`
        : | `Funclass`


Coercions
---------

A name ``f`` can be declared as a coercion between a source user-class
``C`` with `n` parameters and a target class ``D`` if one of these
conditions holds:

 * ``D`` is a user-class, then the type of ``f`` must have the form
   :g:`forall (x₁:A₁)..(xₙ:Aₙ)(y:C x₁..xₙ), D u₁..uₘ` where `m`
   is the number of parameters of ``D``.
 * ``D`` is ``Funclass``, then the type of ``f`` must have the form
   :g:`forall (x₁:A₁)..(xₙ:Aₙ)(y:C x₁..xₙ)(x:A), B`.
 * ``D`` is ``Sortclass``, then the type of ``f`` must have the form
   :g:`forall (x₁:A₁)..(xₙ:Aₙ)(y:C x₁..xₙ), s` with ``s`` a sort.

We then write :g:`f : C >-> D`. The restriction on the type
of coercions is called *the uniform inheritance condition*.

.. note:: The abstract class ``Sortclass`` can be used as a source class, but
{'fraction_non_alphanumeric': 0.15457860615883307, 'fraction_numerical': 0.0, 'mean_word_length': 3.3613074204946995, 'pattern_counts': {'":': 0, '<': 5, '<?xml version=': 0, '>': 9, 'https://': 0, 'lorem ipsum': 0, 'www.': 0, 'xml': 0}, 'pii_count': 0, 'substrings_counts': 0, 'word_list_counts': {'cursed_substrings.json': 0, 'profanity_word_list.json': 0, 'sexual_word_list.json': 0, 'zh_pornsignals.json': 0}}
{'dir': 'git-commits-cleaned', 'id': '7047493', 'n_tokens_mistral': 1700, 'n_tokens_neox': 1644, 'n_words': 747}