Remark: SizeOf instances are automatically generated. We add support for deriving instance for SizeOf just to be able to use them to define instances for types defined at Prelude.lean

def Lean.Elab.Deriving.SizeOf.mkSizeOfHandler (declNames : Array Lake.Name) : Lean.Elab.Command.CommandElabM Bool

Equations

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