Documentation

Lean.Elab.Deriving.SizeOf

source
def Lean.Elab.Deriving.SizeOf.mkSizeOfHandler (declNames : Array Lean.Name) :
Lean.Elab.Command.CommandElabM Bool
Equations
  • One or more equations did not get rendered due to their size.