coercion (uri | term with) [ nat [nat]] [ nocomposites ]

Declares u as an implicit coercion. If the type of u is ∀x1:T1. … ∀x(n-1):T(n-1).Tn the coercion target is T(n - ariety) while its source is T(n - ariety - saturation - 1). Every time a term x of type source is used with expected type target, Matita automatically replaces x with (u ? … ? x ? … ?) to avoid a typing error.

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.