Module docstring

{"# Coercion

Lean uses a somewhat elaborate system of typeclasses to drive the coercion system. Here a coercion means an invisible function that is automatically inserted to fix what would otherwise be a type error. For example, if we have: def f (x : Nat) : Int := x then this is clearly not type correct as is, because x has type Nat but type Int is expected, and normally you will get an error message saying exactly that. But before it shows that message, it will attempt to synthesize an instance of CoeT Nat x Int, which will end up going through all the other typeclasses defined below, to discover that there is an instance of Coe Nat Int defined.

This instance is defined as: instance : Coe Nat Int := ⟨Int.ofNat⟩ so Lean will elaborate the original function f as if it said: def f (x : Nat) : Int := Int.ofNat x which is not a type error anymore.

You can also use the ↑ operator to explicitly indicate a coercion. Using ↑x instead of x in the example will result in the same output.

Because there are many polymorphic functions in Lean, it is often ambiguous where the coercion can go. For example: def f (x y : Nat) : Int := x + y This could be either ↑x + ↑y where + is the addition on Int, or ↑(x + y) where + is addition on Nat, or even x + y using a heterogeneous addition with the type Nat → Nat → Int. You can use the ↑ operator to disambiguate between these possibilities, but generally Lean will elaborate working from the \"outside in\", meaning that it will first look at the expression _ + _ : Int and assign the + to be the one for Int, and then need to insert coercions for the subterms ↑x : Int and ↑y : Int, resulting in the ↑x + ↑y version.

Note that unlike most operators like +, ↑ is always eagerly unfolded at parse time into its definition. So if we look at the definition of f from before, we see no trace of the CoeT.coe function: ``` def f (x : Nat) : Int := x

print f

-- def f : Nat → Int := -- fun (x : Nat) => Int.ofNat x ```

Important typeclasses

Lean resolves a coercion by either inserting a CoeDep instance or chaining CoeHead? CoeOut* Coe* CoeTail? instances. (That is, zero or one CoeHead instances, an arbitrary number of CoeOut instances, etc.)

The CoeHead? CoeOut* instances are chained from the \"left\" side. So if Lean looks for a coercion from Nat to Int, it starts by trying coerce Nat using CoeHead by looking for a CoeHead Nat ?α instance, and then continuing with CoeOut. Similarly Coe* CoeTail? are chained from the \"right\".

These classes should be implemented for coercions:

Coe α β is the most basic class, and the usual one you will want to use when implementing a coercion for your own types. The variables in the type α must be a subset of the variables in β (or out-params of type class parameters), because Coe is chained right-to-left.
CoeOut α β is like Coe α β but chained left-to-right. Use this if the variables in the type α are a superset of the variables in β.
CoeTail α β is like Coe α β, but only applied once. Use this for coercions that would cause loops, like [Ring R] → CoeTail Nat R.
CoeHead α β is similar to CoeOut α β, but only applied once. Use this for coercions that would cause loops, like [SetLike S α] → CoeHead S (Set α).
CoeDep α (x : α) β allows β to depend not only on α but on the value x : α itself. This is useful when the coercion function is dependent. An example of a dependent coercion is the instance for Prop → Bool, because it only holds for Decidable propositions. It is defined as: instance (p : Prop) [Decidable p] : CoeDep Prop p Bool := ...
CoeFun α (γ : α → Sort v) is a coercion to a function. γ a should be a (coercion-to-)function type, and this is triggered whenever an element f : α appears in an application like f x which would not make sense since f does not have a function type. CoeFun instances apply to CoeOut as well.
CoeSort α β is a coercion to a sort. β must be a universe, and this is triggered when a : α appears in a place where a type is expected, like (x : a) or a → a. CoeSort instances apply to CoeOut as well.

On top of these instances this file defines several auxiliary type classes: * CoeTC := Coe* * CoeOTC := CoeOut* Coe* * CoeHTC := CoeHead? CoeOut* Coe* * CoeHTCT := CoeHead? CoeOut* Coe* CoeTail? * CoeDep := CoeHead? CoeOut* Coe* CoeTail? | CoeDep

","# Basic instances ","# Coe bridge "}

Coe structure

(α : semiOutParam (Sort u)) (β : Sort v)

Full source

/--
`Coe α β` is the typeclass for coercions from `α` to `β`. It can be transitively
chained with other `Coe` instances, and coercion is automatically used when
`x` has type `α` but it is used in a context where `β` is expected.
You can use the `↑x` operator to explicitly trigger coercion.
-/
class Coe (α : semiOutParam (Sort u)) (β : Sort v) where
  /-- Coerces a value of type `α` to type `β`. Accessible by the notation `↑x`,
  or by double type ascription `((x : α) : β)`. -/
  coe : α → β

Coercion Typeclass

Informal description

The structure `Coe α β` represents the typeclass for coercions from type `α` to type `β`. It allows for automatic insertion of a coercion function when an element of type `α` is used in a context expecting type `β`. The coercion can be explicitly triggered using the `↑` operator.

CoeTC structure

(α : Sort u) (β : Sort v)

Full source

/--
Auxiliary class implementing `Coe*`.
Users should generally not implement this directly.
-/
class CoeTC (α : Sort u) (β : Sort v) where
  /-- Coerces a value of type `α` to type `β`. Accessible by the notation `↑x`,
  or by double type ascription `((x : α) : β)`. -/
  coe : α → β

Transitive closure of coercions

Informal description

The structure `CoeTC` represents a transitive closure of coercion functions from type `α` to type `β`. It is used internally to implement the coercion system and should not be directly implemented by users. This structure allows for chaining multiple coercions together in a transitive manner.

instCoeTCOfCoe instance

[Coe β γ] [CoeTC α β] : CoeTC α γ

Full source

instance [Coe β γ] [CoeTC α β] : CoeTC α γ where coe a := Coe.coe (CoeTC.coe a : β)

Transitivity of Coercion Closure

Informal description

For any types $\alpha$, $\beta$, and $\gamma$, if there exists a coercion from $\beta$ to $\gamma$ and a transitive closure of coercions from $\alpha$ to $\beta$, then there exists a transitive closure of coercions from $\alpha$ to $\gamma$.

instCoeTCOfCoe_1 instance

[Coe α β] : CoeTC α β

Full source

instance [Coe α β] : CoeTC α β where coe a := Coe.coe a

Transitive Closure of Coercions from Coe

Informal description

For any types $\alpha$ and $\beta$, if there exists a coercion from $\alpha$ to $\beta$, then there exists a transitive closure of coercions from $\alpha$ to $\beta$.

instCoeTC instance

: CoeTC α α

Full source

instance : CoeTC α α where coe a := a

Identity Coercion

Informal description

For any type $\alpha$, there is a trivial coercion from $\alpha$ to itself.

CoeOut structure

(α : Sort u) (β : semiOutParam (Sort v))

Full source

/--
`CoeOut α β` is for coercions that are applied from left-to-right.
-/
class CoeOut (α : Sort u) (β : semiOutParam (Sort v)) where
  /-- Coerces a value of type `α` to type `β`. Accessible by the notation `↑x`,
  or by double type ascription `((x : α) : β)`. -/
  coe : α → β

Left-to-right coercion

Informal description

The structure `CoeOut α β` represents a left-to-right coercion from type `α` to type `β`. It is used when the variables in type `α` are a superset of those in type `β`, ensuring the coercion is applied in the correct direction during type class resolution.

CoeOTC structure

(α : Sort u) (β : Sort v)

Full source

/--
Auxiliary class implementing `CoeOut* Coe*`.
Users should generally not implement this directly.
-/
class CoeOTC (α : Sort u) (β : Sort v) where
  /-- Coerces a value of type `α` to type `β`. Accessible by the notation `↑x`,
  or by double type ascription `((x : α) : β)`. -/
  coe : α → β

Chain of Outward and Basic Coercions

Informal description

The structure `CoeOTC α β` represents a chain of coercions from type `α` to type `β`, consisting of zero or more `CoeOut` instances followed by zero or more `Coe` instances. This auxiliary class is used internally to implement the coercion system and should not be directly implemented by users.

instCoeOTCOfCoeOut instance

[CoeOut α β] [CoeOTC β γ] : CoeOTC α γ

Full source

instance [CoeOut α β] [CoeOTC β γ] : CoeOTC α γ where coe a := CoeOTC.coe (CoeOut.coe a : β)

Composition of Left-to-Right Coercion with Coercion Chain

Informal description

Given types $\alpha$, $\beta$, and $\gamma$, if there exists a left-to-right coercion from $\alpha$ to $\beta$ and a chain of outward and basic coercions from $\beta$ to $\gamma$, then there exists a chain of outward and basic coercions from $\alpha$ to $\gamma$.

instCoeOTCOfCoeTC instance

[CoeTC α β] : CoeOTC α β

Full source

instance [CoeTC α β] : CoeOTC α β where coe a := CoeTC.coe a

Transitive Coercion Closure Implies Coercion Chain

Informal description

For any types $\alpha$ and $\beta$, if there exists a transitive closure of coercions from $\alpha$ to $\beta$, then there exists a chain of outward and basic coercions from $\alpha$ to $\beta$.

instCoeOTC instance

: CoeOTC α α

Full source

instance : CoeOTC α α where coe a := a

Trivial Coercion Chain from a Type to Itself

Informal description

For any type $\alpha$, there is a trivial chain of coercions from $\alpha$ to itself, consisting of zero `CoeOut` and `Coe` instances.

CoeHead structure

(α : Sort u) (β : semiOutParam (Sort v))

Full source

/--
`CoeHead α β` is for coercions that are applied from left-to-right at most once
at beginning of the coercion chain.
-/
class CoeHead (α : Sort u) (β : semiOutParam (Sort v)) where
  /-- Coerces a value of type `α` to type `β`. Accessible by the notation `↑x`,
  or by double type ascription `((x : α) : β)`. -/
  coe : α → β

Head Coercion

Informal description

The structure `CoeHead α β` represents a coercion from type `α` to type `β` that is applied at most once at the beginning of a coercion chain, proceeding from left to right. This is used for coercions that would otherwise cause loops if applied multiple times, such as the coercion from a set-like structure `S` to the type of sets `Set α`.

CoeHTC structure

(α : Sort u) (β : Sort v)

Full source

/--
Auxiliary class implementing `CoeHead CoeOut* Coe*`.
Users should generally not implement this directly.
-/
class CoeHTC (α : Sort u) (β : Sort v) where
  /-- Coerces a value of type `α` to type `β`. Accessible by the notation `↑x`,
  or by double type ascription `((x : α) : β)`. -/
  coe : α → β

Head-Tail Coercion Chain

Informal description

The structure `CoeHTC` represents a chain of coercions consisting of an optional `CoeHead` followed by any number of `CoeOut` and `Coe` instances. This is an auxiliary class used to implement the coercion system in Lean, and users should generally not implement this directly.

instCoeHTCOfCoeHeadOfCoeOTC instance

[CoeHead α β] [CoeOTC β γ] : CoeHTC α γ

Full source

instance [CoeHead α β] [CoeOTC β γ] : CoeHTC α γ where coe a := CoeOTC.coe (CoeHead.coe a : β)

Composition of Head Coercion with Outward-Basic Chain

Informal description

Given types $\alpha$, $\beta$, and $\gamma$, if there exists a head coercion from $\alpha$ to $\beta$ and a chain of outward and basic coercions from $\beta$ to $\gamma$, then there exists a head-tail coercion chain from $\alpha$ to $\gamma$.

instCoeHTCOfCoeOTC instance

[CoeOTC α β] : CoeHTC α β

Full source

instance [CoeOTC α β] : CoeHTC α β where coe a := CoeOTC.coe a

Existence of Head-Tail Coercion Chain from Outward-Basic Chain

Informal description

For any types $\alpha$ and $\beta$, if there exists a chain of outward and basic coercions from $\alpha$ to $\beta$ (i.e., `CoeOTC α β` holds), then there exists a head-tail coercion chain from $\alpha$ to $\beta$ (i.e., `CoeHTC α β` holds).

instCoeHTC instance

: CoeHTC α α

Full source

instance : CoeHTC α α where coe a := a

Reflexivity of Head-Tail Coercion Chains

Informal description

For any type $\alpha$, there is a trivial head-tail coercion chain from $\alpha$ to itself.

CoeTail structure

(α : semiOutParam (Sort u)) (β : Sort v)

Full source

/--
`CoeTail α β` is for coercions that can only appear at the end of a
sequence of coercions. That is, `α` can be further coerced via `Coe σ α` and
`CoeHead τ σ` instances but `β` will only be the expected type of the expression.
-/
class CoeTail (α : semiOutParam (Sort u)) (β : Sort v) where
  /-- Coerces a value of type `α` to type `β`. Accessible by the notation `↑x`,
  or by double type ascription `((x : α) : β)`. -/
  coe : α → β

Tail Coercion

Informal description

The structure `CoeTail α β` represents a coercion from type `α` to type `β` that can only appear at the end of a sequence of coercions. This means that while `α` can be further coerced via `Coe σ α` and `CoeHead τ σ` instances, `β` will be the final expected type of the expression. This is useful for preventing infinite loops in coercion chains.

CoeHTCT structure

(α : Sort u) (β : Sort v)

Full source

/--
Auxiliary class implementing `CoeHead* Coe* CoeTail?`.
Users should generally not implement this directly.
-/
class CoeHTCT (α : Sort u) (β : Sort v) where
  /-- Coerces a value of type `α` to type `β`. Accessible by the notation `↑x`,
  or by double type ascription `((x : α) : β)`. -/
  coe : α → β

Coercion Chain `CoeHead* Coe* CoeTail?`

Informal description

The structure `CoeHTCT` is an auxiliary class that implements the coercion chain `CoeHead* Coe* CoeTail?`, where `CoeHead` is applied zero or one times, followed by any number of `Coe` instances, and optionally followed by one `CoeTail` instance. This class is used internally by Lean's coercion system and is not intended for direct use by users.

instCoeHTCTOfCoeTailOfCoeHTC instance

[CoeTail β γ] [CoeHTC α β] : CoeHTCT α γ

Full source

instance [CoeTail β γ] [CoeHTC α β] : CoeHTCT α γ where coe a := CoeTail.coe (CoeHTC.coe a : β)

Composition of Head-Tail Coercion Chains with Tail Coercion

Informal description

Given types $\alpha$, $\beta$, and $\gamma$, if there exists a tail coercion from $\beta$ to $\gamma$ and a head-tail coercion chain from $\alpha$ to $\beta$, then there exists a head-tail-tail coercion chain from $\alpha$ to $\gamma$.

instCoeHTCTOfCoeHTC instance

[CoeHTC α β] : CoeHTCT α β

Full source

instance [CoeHTC α β] : CoeHTCT α β where coe a := CoeHTC.coe a

Coercion Chain from `CoeHTC` to `CoeHTCT`

Informal description

For any types $\alpha$ and $\beta$, if there exists a chain of coercions from $\alpha$ to $\beta$ consisting of an optional `CoeHead` followed by any number of `CoeOut` and `Coe` instances (i.e., `[CoeHTC α β]` holds), then there exists a corresponding coercion chain of type `CoeHTCT α β$.

instCoeHTCT instance

: CoeHTCT α α

Full source

instance : CoeHTCT α α where coe a := a

Identity Coercion

Informal description

For any type $\alpha$, there is a trivial coercion from $\alpha$ to itself.

CoeDep structure

(α : Sort u) (_ : α) (β : Sort v)

Full source

/--
`CoeDep α (x : α) β` is a typeclass for dependent coercions, that is, the type `β`
can depend on `x` (or rather, the value of `x` is available to typeclass search
so an instance that relates `β` to `x` is allowed).

Dependent coercions do not participate in the transitive chaining process of
regular coercions: they must exactly match the type mismatch on both sides.
-/
class CoeDep (α : Sort u) (_ : α) (β : Sort v) where
  /-- The resulting value of type `β`. The input `x : α` is a parameter to
  the type class, so the value of type `β` may possibly depend on additional
  typeclasses on `x`. -/
  coe : β

Dependent Coercion

Informal description

The structure `CoeDep α (x : α) β` represents a dependent coercion, where the target type `β` can depend on the value `x : α`. Unlike regular coercions, dependent coercions do not participate in transitive chaining and must exactly match the type mismatch on both sides.

CoeT structure

(α : Sort u) (_ : α) (β : Sort v)

Full source

/--
`CoeT` is the core typeclass which is invoked by Lean to resolve a type error.
It can also be triggered explicitly with the notation `↑x` or by double type
ascription `((x : α) : β)`.

A `CoeT` chain has the grammar `CoeHead? CoeOut* Coe* CoeTail? | CoeDep`.
-/
class CoeT (α : Sort u) (_ : α) (β : Sort v) where
  /-- The resulting value of type `β`. The input `x : α` is a parameter to
  the type class, so the value of type `β` may possibly depend on additional
  typeclasses on `x`. -/
  coe : β

Type Coercion System Core

Informal description

The structure `CoeT` represents the core typeclass used by Lean to resolve type errors through coercion. It is triggered either implicitly when a type mismatch occurs or explicitly using the notation `↑x` or double type ascription `((x : α) : β)`. A chain of coercions follows the pattern `CoeHead? CoeOut* Coe* CoeTail? | CoeDep`, where each component handles different aspects of the coercion process.

instCoeTOfCoeHTCT instance

[CoeHTCT α β] : CoeT α a β

Full source

instance [CoeHTCT α β] : CoeT α a β where coe := CoeHTCT.coe a

Coercion from `CoeHTCT` Chains

Informal description

Given types $\alpha$ and $\beta$ with a coercion chain `CoeHead? Coe* CoeTail?` from $\alpha$ to $\beta$, there exists a canonical coercion from any term $a : \alpha$ to type $\beta$.

instCoeTOfCoeDep instance

[CoeDep α a β] : CoeT α a β

Full source

instance [CoeDep α a β] : CoeT α a β where coe := CoeDep.coe a

Dependent Coercion to Core Coercion

Informal description

Given a dependent coercion from type $\alpha$ to type $\beta$ for a specific term $a : \alpha$, there exists a canonical coercion from $a$ to $\beta$ in the typeclass system.

instCoeT instance

: CoeT α a α

Full source

instance : CoeT α a α where coe := a

Trivial Coercion to the Same Type

Informal description

For any type $\alpha$ and term $a : \alpha$, there is a trivial coercion from $a$ to $\alpha$ itself.

CoeFun structure

(α : Sort u) (γ : outParam (α → Sort v))

Full source

/--
`CoeFun α (γ : α → Sort v)` is a coercion to a function. `γ a` should be a
(coercion-to-)function type, and this is triggered whenever an element
`f : α` appears in an application like `f x`, which would not make sense since
`f` does not have a function type.
`CoeFun` instances apply to `CoeOut` as well.
-/
class CoeFun (α : Sort u) (γ : outParam (α → Sort v)) where
  /-- Coerces a value `f : α` to type `γ f`, which should be either be a
  function type or another `CoeFun` type, in order to resolve a mistyped
  application `f x`. -/
  coe : (f : α) → γ f

Function coercion structure

Informal description

The structure `CoeFun α (γ : α → Sort v)` represents a coercion to a function type. Here, for any element `a : α`, `γ a` should be a function type (or a type that can be further coerced to a function type). This coercion is triggered when an element `f : α` appears in a function application `f x` where `f` does not already have a function type. The `γ` parameter is marked as an output parameter, meaning it can be inferred from the context during typeclass resolution.

instCoeOutOfCoeFun instance

[CoeFun α fun _ => β] : CoeOut α β

Full source

instance [CoeFun α fun _ => β] : CoeOut α β where coe a := CoeFun.coe a

Function Coercion Implies Left-to-Right Coercion

Informal description

For any type $\alpha$ and function type $\beta$, if there exists a function coercion from $\alpha$ to $\beta$ (via `CoeFun`), then there also exists a left-to-right coercion from $\alpha$ to $\beta$ (via `CoeOut`).

CoeSort structure

(α : Sort u) (β : outParam (Sort v))

Full source

/--
`CoeSort α β` is a coercion to a sort. `β` must be a universe, and this is
triggered when `a : α` appears in a place where a type is expected, like
`(x : a)` or `a → a`.
`CoeSort` instances apply to `CoeOut` as well.
-/
class CoeSort (α : Sort u) (β : outParam (Sort v)) where
  /-- Coerces a value of type `α` to `β`, which must be a universe. -/
  coe : α → β

Coercion to a sort

Informal description

The structure `CoeSort α β` represents a coercion from a type `α` to a sort `β`, where `β` must be a universe. This coercion is triggered when an element `a : α` appears in a context where a type is expected, such as in type annotations `(x : a)` or function types `a → a`. Instances of `CoeSort` also apply to `CoeOut` coercions.

instCoeOutOfCoeSort instance

[CoeSort α β] : CoeOut α β

Full source

instance [CoeSort α β] : CoeOut α β where coe a := CoeSort.coe a

Coercion to Sort Implies Left-to-Right Coercion

Informal description

For any types $\alpha$ and $\beta$, if there exists a coercion from $\alpha$ to the sort $\beta$, then there also exists a left-to-right coercion from $\alpha$ to $\beta$.

coeNotation definition

: Lean.ParserDescr✝

Full source

/--
`↑x` represents a coercion, which converts `x` of type `α` to type `β`, using
typeclasses to resolve a suitable conversion function. You can often leave the
`↑` off entirely, since coercion is triggered implicitly whenever there is a
type error, but in ambiguous cases it can be useful to use `↑` to disambiguate
between e.g. `↑x + ↑y` and `↑(x + y)`.
-/
syntax:1024 (name := coeNotation) "↑" term:1024 : term

Coercion notation

Informal description

The notation `↑x` represents a coercion that converts a term `x` of type `α` to type `β`, using typeclass resolution to find an appropriate conversion function. This notation can often be omitted, as coercions are automatically inserted to resolve type mismatches. However, in ambiguous cases, explicit use of `↑` can help disambiguate between different possible coercions, such as distinguishing between `↑x + ↑y` and `↑(x + y)`.

coeFunNotation definition

: Lean.ParserDescr✝

Full source

/-- `⇑ t` coerces `t` to a function. -/
syntax:1024 (name := coeFunNotation) "⇑" term:1024 : term

Function coercion notation

Informal description

The notation `⇑ t` represents the coercion of the term `t` to a function. This is used when a term needs to be treated as a function in a context where functions are expected.

coeSortNotation definition

: Lean.ParserDescr✝

Full source

/-- `↥ t` coerces `t` to a type. -/
syntax:1024 (name := coeSortNotation) "↥" term:1024 : term

Type coercion notation

Informal description

The notation `↥ t` represents the coercion of the term `t` to a type. This is used when a term needs to be treated as a type in a context where types are expected.

boolToProp instance

: Coe Bool Prop

Full source

instance boolToProp : Coe Bool Prop where
  coe b := Eq b true

Coercion from Booleans to Propositions

Informal description

The Boolean type `Bool` can be coerced to the type `Prop`, where `true` is interpreted as the true proposition and `false` as the false proposition.

boolToSort instance

: CoeSort Bool Prop

Full source

instance boolToSort : CoeSort Bool Prop where
  coe b := b

Coercion from Booleans to Propositions

Informal description

The Boolean type `Bool` can be coerced to the sort `Prop`, where `true` is interpreted as the true proposition and `false` as the false proposition.

decPropToBool instance

(p : Prop) [Decidable p] : CoeDep Prop p Bool

Full source

instance decPropToBool (p : Prop) [Decidable p] : CoeDep Prop p Bool where
  coe := decide p

Coercion from Decidable Propositions to Booleans

Informal description

For any decidable proposition $p$, there is a dependent coercion from $p$ to the Boolean type `Bool`, where `true` corresponds to $p$ being true and `false` corresponds to $p$ being false.

optionCoe instance

{α : Type u} : Coe α (Option α)

Full source

instance optionCoe {α : Type u} : Coe α (Option α) where
  coe := some

Canonical Coercion from a Type to its Option Type

Informal description

For any type $\alpha$, there is a canonical coercion from $\alpha$ to $\operatorname{Option} \alpha$ that maps an element $x : \alpha$ to $\operatorname{some} x$.

subtypeCoe instance

{α : Sort u} {p : α → Prop} : CoeOut (Subtype p) α

Full source

instance subtypeCoe {α : Sort u} {p : α → Prop} : CoeOut (Subtype p) α where
  coe v := v.val

Subtype Coercion to Base Type

Informal description

For any type $\alpha$ and predicate $p : \alpha \to \text{Prop}$, there is a canonical left-to-right coercion from the subtype $\{x \mid p x\}$ to $\alpha$, which simply forgets the proof that $p$ holds.

Lean.Internal.liftCoeM abbrev

 {m : Type u → Type v} {n : Type u → Type w} {α β : Type u} [MonadLiftT m n] [∀ a, CoeT α a β] [Monad n] (x : m α) : n β

Full source

/--
Helper definition used by the elaborator. It is not meant to be used directly by users.

This is used for coercions between monads, in the case where we want to apply
a monad lift and a coercion on the result type at the same time.
-/
@[coe_decl] abbrev Lean.Internal.liftCoeM {m : Type u → Type v} {n : Type u → Type w} {α β : Type u}
    [MonadLiftT m n] [∀ a, CoeT α a β] [Monad n] (x : m α) : n β := do
  let a ← liftM x
  pure (CoeT.coe a)

Monadic Lift with Coercion: $m \alpha \to n \beta$

Informal description

Given monads $m$ and $n$, types $\alpha$ and $\beta$, and instances of `MonadLiftT m n` and `CoeT α a β` for all $a : \alpha$, the function `liftCoeM` lifts a monadic computation $x : m \alpha$ to a computation in monad $n$ with type $n \beta$. This combines both monad lifting and type coercion in a single operation.

Lean.Internal.coeM abbrev

{m : Type u → Type v} {α β : Type u} [∀ a, CoeT α a β] [Monad m] (x : m α) : m β

Full source

/--
Helper definition used by the elaborator. It is not meant to be used directly by users.

This is used for coercing the result type under a monad.
-/
@[coe_decl] abbrev Lean.Internal.coeM {m : Type u → Type v} {α β : Type u}
    [∀ a, CoeT α a β] [Monad m] (x : m α) : m β := do
  let a ← x
  pure (CoeT.coe a)

Monadic Coercion Lift

Informal description

Given a monad `m` and types `α` and `β` such that for every `a : α` there exists a coercion from `α` to `β` via `CoeT`, and given a monadic value `x : m α`, the function `coeM` lifts `x` to a monadic value of type `m β` by applying the coercion under the monad.