Documentation

Std.Tactic.CoeExt

inductive Std.Tactic.Coe.CoeFnType :

The basic coercion ↑x↑x, see CoeT.coe
coe: Std.Tactic.Coe.CoeFnType
The coercion to a function type, see CoeFun.coe
coeFun: Std.Tactic.Coe.CoeFnType
The coercion to a type, see CoeSort.coe
coeSort: Std.Tactic.Coe.CoeFnType

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

Instances For

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 :

The number of arguments to the coercion function
numArgs : Nat
The argument index that represents the value being coerced
coercee : Nat
The type of coercion
type : Std.Tactic.Coe.CoeFnType

Information associated to a coercion function to enable sensible delaboration.

Instances For

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↑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)