Defines notations for coercions.

`↑ t`

is defined in core.`(↑)`

is equivalent to the eta-reduction of`(↑ ·)`

`⇑ t`

is a coercion to a function type.`(⇑)`

is equivalent to the eta-reduction of`(⇑ ·)`

`↥ t`

is a coercion to a type.`(↥)`

is equivalent to the eta-reduction of`(↥ ·)`

def
Lean.Elab.Term.CoeImpl.elabPartiallyAppliedCoe
(sym : String)
(expectedType : Lean.Expr)
(mkCoe : Lean.Expr → Lean.Expr → Lean.Elab.TermElabM Lean.Expr)
:

Elaborator for the `(↑)`

, `(⇑)`

, and `(↥)`

notations.

## Equations

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

## Instances For

Partially applied coercion. Equivalent to the η-reduction of `(↑ ·)`

## Equations

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

## Instances For

Partially applied function coercion. Equivalent to the η-reduction of `(⇑ ·)`

## Equations

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

## Instances For

Partially applied type coercion. Equivalent to the η-reduction of `(↥ ·)`

## Equations

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