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.instInhabitedCoeFnType.default }

def Lean.Meta.instInhabitedCoeFnType.default : CoeFnType

Equations

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

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✝

instance Lean.Meta.instReprCoeFnType : Repr CoeFnType

Equations

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

instance Lean.Meta.instDecidableEqCoeFnType : DecidableEq CoeFnType

Equations

• Lean.Meta.instDecidableEqCoeFnType x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx 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 := Lean.Meta.instInhabitedCoeFnInfo.default }

def Lean.Meta.instInhabitedCoeFnInfo.default : 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.instReprCoeFnInfo.repr }

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

Equations

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

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.