diff --git a/src/Init/Data/Char/Basic.lean b/src/Init/Data/Char/Basic.lean index f163ef8ed7..58a4de6774 100644 --- a/src/Init/Data/Char/Basic.lean +++ b/src/Init/Data/Char/Basic.lean @@ -9,8 +9,6 @@ import Init.Data.UInt @[inline, reducible] def isValidChar (n : UInt32) : Prop := n < 0xd800 ∨ (0xdfff < n ∧ n < 0x110000) -instance : SizeOf Char := ⟨fun c => c.val.toNat⟩ - namespace Char protected def Less (a b : Char) : Prop := a.val < b.val diff --git a/src/Init/Data/String/Basic.lean b/src/Init/Data/String/Basic.lean index cb05a6e7a0..0b9651c4a2 100644 --- a/src/Init/Data/String/Basic.lean +++ b/src/Init/Data/String/Basic.lean @@ -153,8 +153,6 @@ def splitOn (s : String) (sep : String := " ") : List String := instance : Inhabited String := ⟨""⟩ -instance : SizeOf String := ⟨String.length⟩ - instance : Append String := ⟨String.append⟩ def str : String → Char → String := push