Documentation

Lean.Meta.Instances

Instances For
Equations
Equations
Equations
  • One or more equations did not get rendered due to their size.
Equations
def Lean.Meta.Instances.erase {m : TypeType} [Monad m] [MonadError m] (d : Instances) (declName : Name) :
Equations
  • One or more equations did not get rendered due to their size.
def Lean.Meta.addInstance (declName : Name) (attrKind : AttributeKind) (prio : Nat) :
Equations
  • One or more equations did not get rendered due to their size.
Equations
Equations
  • One or more equations did not get rendered due to their size.
Equations
  • One or more equations did not get rendered due to their size.

Default instance support #

@[reducible, inline]
Equations
Equations
  • One or more equations did not get rendered due to their size.
def Lean.Meta.addDefaultInstance (declName : Name) (prio : Nat := 0) :
Equations
  • One or more equations did not get rendered due to their size.
def Lean.Meta.getDefaultInstances {m : TypeType} [Monad m] [MonadEnv m] (className : Name) :
m (List (Name × Nat))
Equations