# The `@[coe]` attribute, used to delaborate coercion functions as `↑` #

When writing a coercion, if the pattern

    @[coe]
    def A.toB (a : A) : B := sorry

    instance : Coe A B where coe := A.toB

is used, then `A.toB a` will be pretty-printed as `↑a`.

source
inductive Lean.Meta.CoeFnType :
Type

The different types of coercions that are supported by the `coe` attribute.

- coe : CoeFnType

  The basic coercion `↑x`, see `CoeT.coe`

- coeFun : CoeFnType

  The coercion to a function type, see `CoeFun.coe`

- coeSort : CoeFnType

  The coercion to a type, see `CoeSort.coe`

Instances For

source
def Lean.Meta.instInhabitedCoeFnType.default :
CoeFnType
Equations

- Lean.Meta.instInhabitedCoeFnType.default = Lean.Meta.CoeFnType.coe

Instances For

source
instance Lean.Meta.instInhabitedCoeFnType :
Inhabited CoeFnType
Equations

- Lean.Meta.instInhabitedCoeFnType = { default := Lean.Meta.instInhabitedCoeFnType.default }

source
instance Lean.Meta.instReprCoeFnType :
Repr CoeFnType
Equations

- Lean.Meta.instReprCoeFnType = { reprPrec := Lean.Meta.instReprCoeFnType.repr }

source
def Lean.Meta.instReprCoeFnType.repr :
CoeFnType → Nat → Format
Equations

- One or more equations did not get rendered due to their size.
- Lean.Meta.instReprCoeFnType.repr Lean.Meta.CoeFnType.coe prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Lean.Meta.CoeFnType.coe")).group prec✝
- Lean.Meta.instReprCoeFnType.repr Lean.Meta.CoeFnType.coeFun prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Lean.Meta.CoeFnType.coeFun")).group prec✝

Instances For

source
instance Lean.Meta.instDecidableEqCoeFnType :
DecidableEq CoeFnType
Equations

- Lean.Meta.instDecidableEqCoeFnType x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

source
instance Lean.Meta.instToExprCoeFnType :
ToExpr CoeFnType
Equations

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

source
structure Lean.Meta.CoeFnInfo :
Type

Information associated to a coercion function to enable sensible delaboration.

- numArgs : Nat

  The number of arguments to the coercion function

- coercee : Nat

  The argument index that represents the value being coerced

- type : CoeFnType

  The type of coercion

Instances For

source
instance Lean.Meta.instInhabitedCoeFnInfo :
Inhabited CoeFnInfo
Equations

- Lean.Meta.instInhabitedCoeFnInfo = { default := Lean.Meta.instInhabitedCoeFnInfo.default }

source
def Lean.Meta.instInhabitedCoeFnInfo.default :
CoeFnInfo
Equations

- Lean.Meta.instInhabitedCoeFnInfo.default = { numArgs := default, coercee := default, type := default }

Instances For

source
instance Lean.Meta.instReprCoeFnInfo :
Repr CoeFnInfo
Equations

- Lean.Meta.instReprCoeFnInfo = { reprPrec := Lean.Meta.instReprCoeFnInfo.repr }

source
def Lean.Meta.instReprCoeFnInfo.repr :
CoeFnInfo → Nat → Format
Equations

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

Instances For

source
instance Lean.Meta.instToExprCoeFnInfo :
ToExpr CoeFnInfo
Equations

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

source
opaque Lean.Meta.coeExt :
SimpleScopedEnvExtension (Name × CoeFnInfo) (NameMap CoeFnInfo)

The environment extension for tracking coercion functions for delaboration

source
def Lean.Meta.getCoeFnInfo? (fn : Name) :
CoreM (Option CoeFnInfo)

Lookup the coercion information for a given function

Equations

- Lean.Meta.getCoeFnInfo? fn = do let __do_lift ← Lean.getEnv pure ((Lean.ScopedEnvExtension.getState Lean.Meta.coeExt __do_lift).find? fn)

Instances For

source
def Lean.Meta.registerCoercion (name : Name) (info : Option CoeFnInfo := none) :
MetaM Unit

Add `name` to the coercion extension and add a coercion delaborator for the function.

Equations

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

Instances For