From 46c62a3fedf00667970a42be2040cbbd3f2be081 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Wed, 20 Jan 2021 17:50:43 -0800 Subject: [PATCH] chore: add missing instances --- src/Init/SizeOf.lean | 10 ++++++++-- 1 file changed, 8 insertions(+), 2 deletions(-) diff --git a/src/Init/SizeOf.lean b/src/Init/SizeOf.lean index d81daaa75c..5658145c41 100644 --- a/src/Init/SizeOf.lean +++ b/src/Init/SizeOf.lean @@ -35,10 +35,16 @@ deriving instance SizeOf for Option deriving instance SizeOf for List deriving instance SizeOf for Array deriving instance SizeOf for Subtype -deriving instance SizeOf for Except -deriving instance SizeOf for EStateM.Result +deriving instance SizeOf for Fin +deriving instance SizeOf for USize +deriving instance SizeOf for UInt8 +deriving instance SizeOf for UInt16 +deriving instance SizeOf for UInt32 +deriving instance SizeOf for UInt64 deriving instance SizeOf for Char deriving instance SizeOf for String deriving instance SizeOf for Substring +deriving instance SizeOf for Except +deriving instance SizeOf for EStateM.Result deriving instance SizeOf for Lean.Name deriving instance SizeOf for Lean.Syntax