chore: remove old instances
This commit is contained in:
parent
7c6d09496e
commit
e8401ea6e7
2 changed files with 0 additions and 4 deletions
|
|
@ -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
|
||||
|
|
|
|||
|
|
@ -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
|
||||
|
|
|
|||
Loading…
Add table
Reference in a new issue