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: Lean.Meta.CoeFnType

  The basic coercion ↑x, see CoeT.coe

• coeFun: Lean.Meta.CoeFnType

  The coercion to a function type, see CoeFun.coe

• coeSort: Lean.Meta.CoeFnType

  The coercion to a type, see CoeSort.coe

instance Lean.Meta.instInhabitedCoeFnType : Inhabited Lean.Meta.CoeFnType

Equations

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

instance Lean.Meta.instReprCoeFnType : Repr Lean.Meta.CoeFnType

Equations

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

instance Lean.Meta.instDecidableEqCoeFnType : DecidableEq Lean.Meta.CoeFnType

Equations

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

instance Lean.Meta.instToExprCoeFnType : Lean.ToExpr Lean.Meta.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 : Lean.Meta.CoeFnType

  The type of coercion

instance Lean.Meta.instInhabitedCoeFnInfo : Inhabited Lean.Meta.CoeFnInfo

Equations

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

instance Lean.Meta.instReprCoeFnInfo : Repr Lean.Meta.CoeFnInfo

Equations

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

instance Lean.Meta.instToExprCoeFnInfo : Lean.ToExpr Lean.Meta.CoeFnInfo

Equations

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

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

The environment extension for tracking coercion functions for delaboration

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

Lookup the coercion information for a given function

Equations

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

def Lean.Meta.registerCoercion (name : Lake.Name) (info : optParam (Option Lean.Meta.CoeFnInfo) none) : Lean.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.