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

Equations

• Lean.Meta.instInhabitedCoeFnType = { default := Lean.Meta.CoeFnType.coe }

instance Lean.Meta.instReprCoeFnType : Repr CoeFnType

Equations

• Lean.Meta.instReprCoeFnType = { reprPrec := Lean.Meta.reprCoeFnType✝ }

instance Lean.Meta.instDecidableEqCoeFnType : DecidableEq CoeFnType

Equations

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

instance Lean.Meta.instToExprCoeFnType : ToExpr CoeFnType

Equations

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

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

Equations

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

instance Lean.Meta.instReprCoeFnInfo : Repr CoeFnInfo

Equations

• Lean.Meta.instReprCoeFnInfo = { reprPrec := Lean.Meta.reprCoeFnInfo✝ }

instance Lean.Meta.instToExprCoeFnInfo : ToExpr CoeFnInfo

Equations

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

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

Equations

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

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.