The type Even represents the even natural numbers.

A coercion allows even numbers to be used where natural numbers are expected. The coe attribute marks the projection as a coercion so that it can be shown accordingly in proof states and error messages, as described in the section on implementing coercions.

With this coercion in place, even numbers can be used where natural numbers are expected.

5

Due to coercion chaining, there is also a coercion from Even to Int formed by chaining the Coe Even Nat instance with the existing coercion from Nat to Int:

-1

The string "four" can be coerced into the natural number 4 with this instance declaration:

4

Ordinary type errors are produced for other strings:

type mismatch
  "three"
has type
  String : Type
but is expected to have type
  Nat : Type

A Truthy value is a value paired with an indication of whether it should be considered to be true or false. A Decision is either yes, no, or maybe, with the latter containing further data for consideration.

“Truthy” values can be converted to Bools by forgetting the contained value. Bools can be converted to Decisions by discounting the maybe case.

Truthy.toBool must be a CoeOut instance, because the target of the coercion contains fewer unknown type variables than the source, while Decision.ofBool must be a Coe instance, because the source of the coercion contains fewer variables than the target:

With these instances, coercion chaining works:

Decision.yes

Attempting to use the wrong class leads to an error:

instance does not provide concrete values for (semi-)out-params
  Coe (Truthy ?α) Bool

A type of non-empty lists can be defined as a pair of a list and a proof that it is not empty. This type can be coerced to ordinary lists by applying the projection:

The coercion works as expected:

Arbitrary lists cannot, however, be coerced to non-empty lists, because some arbitrarily-chosen lists may indeed be empty:

don't know how to synthesize placeholder for argument 'non_empty'
context:
α : Type u_1
xs : List α
⊢ xs ≠ []

A dependent coercion can restrict the domain of the coercion to only lists that are not empty:

{ contents := [1, 2, 3], non_empty := _ }

Dependent coercion insertion requires that the term to be coerced syntactically matches the term in the instance header. Lists that are known to be non-empty, but which are not syntactically instances of (· :: ·), cannot be coerced with this instance.

When coercion insertion fails, the original type error is reported:

type mismatch
  ys
has type
  List Nat : Type
but is expected to have type
  NonEmptyList Nat : Type

Instance synthesis and coercion insertion interact with one another. Synthesizing an instance may make type information known that later triggers coercion insertion. The specific placement of coercions may matter.

In this definition of sub, the Sub Int instance is synthesized based on the function's return type. This instance requires that the two parameters also be Ints, but they are Nats. Coercions are inserted around each argument to the subtraction operator. This can be seen in the output of Lean.Parser.Command.print : command#print.

def sub : Nat → Nat → Int :=
fun n k => ↑n - ↑k

Placing the coercion operator outside the subtraction causes the elaborator to attempt to infer a type for the subtraction and then insert a coercion. Because the arguments are both Nats, the Sub Nat instance is selected, leading to the difference being a Nat. The difference is then coerced to an Int.

These two functions are not equivalent because subtraction of natural numbers truncates at zero:

-4

0