The structure Later represents a term that can be evaluated in the future, by calling the contained function.

A coercion from any value to a later value is performed by creating a function that wraps it.

However, if coercion insertion resulted in an application of CoeTail.coe, then this coercion would not have the desired effect at runtime, because the coerced value would be evaluated and then saved in the function's closure. Because coercion implementations are unfolded, this instance is nonetheless useful.

Printing the resulting definition shows that the computation is inside the function's body:

def tomorrow : Later String :=
{ get := fun x => Nat.fold 10000 (fun x x s => s ++ "tomorrow") "" }

Because the contents of Coe instances are unfolded during coercion insertion, coercions that use their argument more than once should be careful to ensure that evaluation occurs just once. This can be done by using a helper function that is not part of the instance, or by using Lean.Parser.Term.let : term`let` is used to declare a local definition. Example: ``` let x := 1 let y := x + 1 x + y ``` Since functions are first class citizens in Lean, you can use `let` to declare local functions too. ``` let double := fun x => 2*x double (double 3) ``` For recursive definitions, you should use `let rec`. You can also perform pattern matching using `let`. For example, assume `p` has type `Nat × Nat`, then you can write ``` let (x, y) := p x + y ``` let to evaluate the coerced term and then re-use its resulting value.

The structure Twice requires that both fields have the same value:

One way to define a coercion from α to Twice α is with a helper function twice. The coe attribute marks it as a coercion so it can be shown correctly in proof goals and error messages.

When the Coe instance is unfolded, the call to twice remains, which causes its argument to be evaluated before the body of the function is executed. As a result, the Lean.Parser.Term.dbgTrace : term`dbg_trace e; body` evaluates to `body` and prints `e` (which can be an interpolated string literal) to stderr. It should only be used for debugging. dbg_trace executes just once:

hello

{ first := 5, second := 5, first_eq_second := _ }

Inlining the helper into the Coe instance results in a term that duplicates the Lean.Parser.Term.dbgTrace : term`dbg_trace e; body` evaluates to `body` and prints `e` (which can be an interpolated string literal) to stderr. It should only be used for debugging. dbg_trace:

hello
hello

{ first := 5, second := 5, first_eq_second := _ }

Introducing an intermediate name for the result of the evaluation prevents the duplicated work:

hello

{ first := 5, second := 5, first_eq_second := _ }

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

A monoid is a type equipped with an associative binary operation and an identity element. While monoid structure can be defined as a type class, it can also be defined as a structure that “bundles up” the structure with the type:

The type Monoid does not indicate the carrier:

However, a CoeSort instance can be implemented that applies the Monoid.Carrier projection when a monoid is used in a position where Lean would expect a type:

The inductive type NatOrBool represents the types Nat and Bool. The can be coerced to the actual types Nat and Bool:

The CoeSort instance is used when nat occurs to the right of a colon:

When an expected type is available, ordinary coercion insertion is used. In this case, the CoeSort instance is used to synthesize a CoeOut NatOrBool Type instance, which chains with the Coe Type (Option Type) instance to recover from the type error.

The structure NamedFun α β pairs a function from α to β with a name.

Existing functions can be named:

Named functions can also be composed:

Unlike ordinary functions, named functions have a reasonable representation as a string:

#<asString ∘ succ>

A CoeFun instance allows them to be applied just like ordinary functions:

[1, 2, 3, 4, 5, 6]

Sometimes, the type of the resulting function depends on the specific value that is being coerced. A Writer represents a means of appending a representation of some value to a string:

Because the type of the parameter expected by the inner function depend on the Writer.Writes field, the CoeFun instance extracts the field:

With this instance, concrete Writers can be used as functions:

"5 hello"

A well-typed interpreter is an interpreter for a programming language that uses indexed families to rule out run-time type errors. Functions written in the interpreted language can be interpreted as Lean functions, but their underlying source code can also be inspected.

The first step in the well-typed interpreter is to select the subset of Lean types that can be used. These types are represented by an inductive type of codes Ty and a function that maps these codes to actual types.

The language itself is represented by an indexed family over variable contexts and result types. Variables are represented by de Bruijn indices.

Because the OfNat instance for Fin requires that the upper bound be non-zero, Tm.var can be inconvenient to use with numeric literals. The helper Tm.v can be used to avoid the need for type annotations in these cases.

A function that adds two natural numbers uses the rep operation to apply the successor Tm.succ repeatedly.

Each typing context can be interpreted as a type of run-time environments that provide a value for each variable in the context:

Finally, the interpreter is a recursive function over the term:

Coercing a Tm to a function consists of calling the interpreter.

Because functions are represented by a first-order inductive type, their code can be inspected:

Tm.lam (Tm.lam (Tm.rep (Tm.var 1) (Tm.var 0) (Tm.lam (Tm.lam (Tm.succ (Tm.var 0))))))

At the same time, due to the coercion, they can be applied just like native Lean functions:

8