# Documentation

Std.Tactic.CoeExt

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

Instances For
Equations
Equations
Equations
• One or more equations did not get rendered due to their size.
• 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

Information associated to a coercion function to enable sensible delaboration.

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

The environment extension for tracking coercion functions for delaboration

Lookup the coercion information for a given function

Equations
• = do let __do_lift ← Lean.getEnv pure ()

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.

Add a coercion delaborator for the given function.

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

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.

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