- coe: Std.Tactic.Coe.CoeFnType
The basic coercion
↑x
, seeCoeT.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.
Instances For
- 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.
Instances For
The environment extension for tracking coercion functions for delaboration
Lookup the coercion information for a given function
Instances For
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.
Instances For
Add a coercion delaborator for the given function.
Instances For
Add name
to the coercion extension and add a coercion delaborator for the function.
Instances For
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.