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.

This file also provides ⇑f and ↥t notation, which are syntax for Lean.Meta.coerceToFunction? and Lean.Meta.coerceToSort? respectively.

def Std.Tactic.Coe.coeFunNotation : Lean.ParserDescr

⇑ t coerces t to a function.

Equations

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

def Std.Tactic.Coe.coeSortNotation : Lean.ParserDescr

↥ t coerces t to a type.

Equations

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

inductive Std.Tactic.Coe.CoeFnType : Type

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

• 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

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

Equations

• Std.Tactic.Coe.instInhabitedCoeFnType = { default := Std.Tactic.Coe.CoeFnType.coe }

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

Equations

• Std.Tactic.Coe.instReprCoeFnType = { reprPrec := Std.Tactic.Coe.reprCoeFnType✝ }

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

Equations

• Std.Tactic.Coe.instDecidableEqCoeFnType x y = if h : Std.Tactic.Coe.CoeFnType.toCtorIdx x = Std.Tactic.Coe.CoeFnType.toCtorIdx y then isTrue (_ : x = y) else isFalse (_ : x = y → False)

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

Equations

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

structure Std.Tactic.Coe.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 : Std.Tactic.Coe.CoeFnType

  The type of coercion

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

Equations

• Std.Tactic.Coe.instInhabitedCoeFnInfo = { default := { numArgs := default, coercee := default, type := default } }

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

Equations

• Std.Tactic.Coe.instReprCoeFnInfo = { reprPrec := Std.Tactic.Coe.reprCoeFnInfo✝ }

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

Equations

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

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

Equations

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

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.

Equations

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

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

Add a coercion delaborator for the given function.

Equations

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

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.

Equations

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

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.

Equations

• Std.Tactic.Coe.Attr.coe = Lean.ParserDescr.node `Std.Tactic.Coe.Attr.coe 1024 (Lean.ParserDescr.nonReservedSymbol "coe" false)