Return true iff `declName`

is one of the auxiliary definitions/projections
used to implement coercions.

## Equations

- Lean.Meta.isCoeDecl env declName = Lean.TagAttribute.hasTag Lean.Meta.coeDeclAttr env declName

Expand coercions occurring in `e`

## Equations

- One or more equations did not get rendered due to their size.

Coerces `expr`

to `expectedType`

using `CoeT`

.

## Equations

- One or more equations did not get rendered due to their size.

Coerces `expr`

to a function type.

## Equations

- One or more equations did not get rendered due to their size.

Coerces `expr`

to a type.

## Equations

- One or more equations did not get rendered due to their size.

Return `some (m, α)`

if `type`

can be reduced to an application of the form `m α`

using `[reducible]`

transparency.

## Equations

- One or more equations did not get rendered due to their size.

Return `true`

if `type`

is of the form `m α`

where `m`

is a `Monad`

.
Note that we reduce `type`

using transparency `[reducible]`

.

## Equations

- One or more equations did not get rendered due to their size.

Try coercions and monad lifts to make sure `e`

has type `expectedType`

.

If `expectedType`

is of the form `n β`

, we try monad lifts and other extensions.

Extensions for monads.

- Try to unify
`n`

and`m`

. If it succeeds, then we use

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

`n`

must be a `Monad`

to use this one.

- If there is monad lift from
`m`

to`n`

and we can unify`α`

and`β`

, we use

```
liftM : ∀ {m : Type u_1 → Type u_2} {n : Type u_1 → Type u_3} [self : MonadLiftT m n] {α : Type u_1}, m α → n α
∀ {m : Type u_1 → Type u_2} {n : Type u_1 → Type u_3} [self : MonadLiftT m n] {α : Type u_1}, m α → n α
→ Type u_2} {n : Type u_1 → Type u_3} [self : MonadLiftT m n] {α : Type u_1}, m α → n α
→ Type u_3} [self : MonadLiftT m n] {α : Type u_1}, m α → n α
→ n α
```

Note that `n`

may not be a `Monad`

in this case. This happens quite a bit in code such as

```
def g (x : Nat) : IO Nat := do
IO.println x
pure x
def f {m} [MonadLiftT IO m] : m Nat :=
g 10
```

- If there is a monad lift from
`m`

to`n`

and a coercion from`α`

to`β`

, we use

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

Note that approach 3 does not subsume 1 because it is only applicable if there is a coercion from `α`

to `β`

for all values in `α`

.
This is not the case for example for `pure $ x > 0`

when the expected type is `IO Bool`

. The given type is `IO Prop`

, and
we only have a coercion from decidable propositions. Approach 1 works because it constructs the coercion `CoeT (m Prop) (pure $ x > 0) (m Bool)`

using the instance `pureCoeDepProp`

.

Note that, approach 2 is more powerful than `tryCoe`

.
Recall that type class resolution never assigns metavariables created by other modules.
Now, consider the following scenario

```
def g (x : Nat) : IO Nat := ...
deg h (x : Nat) : StateT Nat IO Nat := do
v ← g x;
IO.Println v;
...
← g x;
IO.Println v;
...
```

Let's assume there is no other occurrence of `v`

in `h`

.
Thus, we have that the expected of `g x`

is `StateT Nat IO ?α`

,
and the given type is `IO Nat`

. So, even if we add a coercion.

```
instance {α m n} [MonadLiftT m n] {α} : Coe (m α) (n α) := ...
```

It is not applicable because TC would have to assign `?α := Nat`

.
On the other hand, TC can easily solve `[MonadLiftT IO (StateT Nat IO)]`

since this goal does not contain any metavariables. And then, we
convert `g x`

into `liftM $ g x`

.

## Equations

- One or more equations did not get rendered due to their size.

Coerces `expr`

to the type `expectedType`

.
Returns `.some coerced`

on successful coercion,
`.none`

if the expression cannot by coerced to that type,
or `.undef`

if we need more metavariable assignments.

## Equations

- One or more equations did not get rendered due to their size.