Documentation

Lean.Elab.Deriving.SizeOf

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

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.
Instances For