- keys : Array InstanceKey
- val : Expr
- priority : Nat
The order in which the instance's arguments are to be synthesized.
- attrKind : AttributeKind
Instances For
- discrTree : InstanceTree
- instanceNames : PHashMap Name InstanceEntry
Instances For
Equations
Instances For
Equations
Instances For
def
Lean.Meta.Instances.erase
{m : Type → Type}
[Monad m]
[MonadError m]
(d : Instances)
(declName : Name)
:
Equations
Instances For
Equations
Instances For
Equations
Instances For
Equations
Instances For
Default instance support #
- priorities : PrioritySet