Matita Home

`coercion nocomposites c : ty ≝ u on s : S to T`

- Synopsis:
**coercion**[**nocomposites**]*id*[ :*term***≝***term***on***id*:*term***to***term*]- Action:
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.