inductive Std.Tactic.Coe.CoeFnType : Type

• coe: Std.Tactic.Coe.CoeFnType

  The basic coercion ↑x, see CoeT.coe

• coeFun: Std.Tactic.Coe.CoeFnType

  The coercion to a function type, see CoeFun.coe

• coeSort: Std.Tactic.Coe.CoeFnType

  The coercion to a type, see CoeSort.coe

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

instance Std.Tactic.Coe.instInhabitedCoeFnType : Inhabited Std.Tactic.Coe.CoeFnType

instance Std.Tactic.Coe.instReprCoeFnType : Repr Std.Tactic.Coe.CoeFnType

instance Std.Tactic.Coe.instDecidableEqCoeFnType : DecidableEq Std.Tactic.Coe.CoeFnType

instance Std.Tactic.Coe.instToExprCoeFnType : Lean.ToExpr Std.Tactic.Coe.CoeFnType

structure Std.Tactic.Coe.CoeFnInfo : Type

• numArgs : Nat

  The number of arguments to the coercion function

• coercee : Nat

  The argument index that represents the value being coerced

• type : Std.Tactic.Coe.CoeFnType

  The type of coercion

Information associated to a coercion function to enable sensible delaboration.

instance Std.Tactic.Coe.instInhabitedCoeFnInfo : Inhabited Std.Tactic.Coe.CoeFnInfo

instance Std.Tactic.Coe.instReprCoeFnInfo : Repr Std.Tactic.Coe.CoeFnInfo

instance Std.Tactic.Coe.instToExprCoeFnInfo : Lean.ToExpr Std.Tactic.Coe.CoeFnInfo

opaque Std.Tactic.Coe.coeExt : Lean.SimpleScopedEnvExtension (Lean.Name × Std.Tactic.Coe.CoeFnInfo) (Lean.NameMap Std.Tactic.Coe.CoeFnInfo)

The environment extension for tracking coercion functions for delaboration

def Std.Tactic.Coe.getCoeFnInfo? (fn : Lean.Name) : Lean.CoreM (Option Std.Tactic.Coe.CoeFnInfo)

Lookup the coercion information for a given function

def Std.Tactic.Coe.coeDelaborator (info : Std.Tactic.Coe.CoeFnInfo) : Lean.PrettyPrinter.Delaborator.Delab

This delaborator tries to elide functions which are known coercions. For example, Int.ofNat is a coercion, so instead of printing ofNat n we just print ↑n, and when re-parsing this we can (usually) recover the specific coercion being used.

def Std.Tactic.Coe.addCoeDelaborator (name : Lean.Name) (info : Std.Tactic.Coe.CoeFnInfo) : Lean.MetaM Unit

Add a coercion delaborator for the given function.

def Std.Tactic.Coe.registerCoercion (name : Lean.Name) (info : optParam (Option Std.Tactic.Coe.CoeFnInfo) none) : Lean.MetaM Unit

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

def Std.Tactic.Coe.Attr.coe : Lean.ParserDescr

The @[coe] attribute on a function (which should also appear in a instance : Coe A B := ⟨myFn⟩ declaration) allows the delaborator to show applications of this function as ↑ when printing expressions.