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.

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

instance Lean.Meta.instInhabitedCoeFnType : Inhabited CoeFnType

instance Lean.Meta.instReprCoeFnType : Repr CoeFnType

instance Lean.Meta.instDecidableEqCoeFnType : DecidableEq CoeFnType

instance Lean.Meta.instToExprCoeFnType : ToExpr CoeFnType

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

instance Lean.Meta.instInhabitedCoeFnInfo : Inhabited CoeFnInfo

instance Lean.Meta.instReprCoeFnInfo : Repr CoeFnInfo

instance Lean.Meta.instToExprCoeFnInfo : ToExpr CoeFnInfo

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

The environment extension for tracking coercion functions for delaboration

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

Lookup the coercion information for a given function

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.