coercion [ nocomposites ] id [ : term ≝ term on id : term to term ]

Declares c as an implicit coercion. If only c is given, u is the constant named by c, ty its declared type, s the name of the last variable abstracted in in ty, S the type of this last variable and T the target of ty. The user can specify all these component to have full control on how the coercion is indexed. The type of the body of the coercion u must be convertible to the declared one ty. Let it be ∀x1:T1. … ∀x(n-1):T(n-1).Tn. Then s must be one of x1 … xn (possibly prefixed by _ if the product is non dependent). Let s be xi in the following. Then S must be Ti where all bound variables are replaced by ?, and T must be Tn where all bound variable are replaced by ?. For example the following command declares a coercions from vectors of any length to lists of natural numbers.

coercion nocomposites v2l : ∀n:nat.∀v:Vect nat n. List nat ≝ l_of_v on _v : Vect nat ? to List nat

Every time a term x of a type that matches S (Vect nat ? here) is used with an expected type that matches T (List nat here), Matita automatically replaces x with (u ? … ? x ? … ?) to avoid a typing error. Note that the position of x is determined by s.

Implicit coercions are not displayed to the user: (u ? … ? x) is rendered simply as x.

When a coercion u is declared from source s to target t and there is already a coercion u' of target s or source t, a composite implicit coercion is automatically computed by Matita unless nocomposites is specified.

Note that Vect nat ? can be replaced with Vect ? ? to index the coercion is a loose way.