From f6556ecdccdc7f324d348b758667e640af7e2d33 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Sat, 15 Apr 2017 22:48:42 -0700
Subject: [PATCH] fix(library/init): missing has_sizeof instances for subtype,
 char and string

---
 library/init/core.lean              | 6 ++++++
 library/init/data/char/basic.lean   | 3 +++
 library/init/data/string/basic.lean | 3 +++
 3 files changed, 12 insertions(+)

diff --git a/library/init/core.lean b/library/init/core.lean
index 0d006fbd6c..8b7ff90c84 100644
--- a/library/init/core.lean
+++ b/library/init/core.lean
@@ -592,6 +592,12 @@ protected def list.sizeof {α : Type u} [has_sizeof α] : list α → nat
 instance (α : Type u) [has_sizeof α] : has_sizeof (list α) :=
 ⟨list.sizeof⟩
 
+protected def subtype.sizeof {α : Type u} [has_sizeof α] {p : α → Prop} : subtype p → nat
+| ⟨a, _⟩ := sizeof a
+
+instance {α : Type u} [has_sizeof α] (p : α → Prop) : has_sizeof (subtype p) :=
+⟨subtype.sizeof⟩
+
 lemma nat_add_zero (n : nat) : n + 0 = n := rfl
 
 /- Combinator calculus -/
diff --git a/library/init/data/char/basic.lean b/library/init/data/char/basic.lean
index 2cbf476499..a95b7b8998 100644
--- a/library/init/data/char/basic.lean
+++ b/library/init/data/char/basic.lean
@@ -11,6 +11,9 @@ def char_sz : nat := succ 255
 
 def char := fin char_sz
 
+instance : has_sizeof char :=
+⟨fin.sizeof _⟩
+
 namespace char
 /- We cannot use tactic dec_trivial here because the tactic framework has not been defined yet. -/
 lemma zero_lt_char_sz : 0 < char_sz :=
diff --git a/library/init/data/string/basic.lean b/library/init/data/string/basic.lean
index b52fd151ad..16940093ec 100644
--- a/library/init/data/string/basic.lean
+++ b/library/init/data/string/basic.lean
@@ -15,6 +15,9 @@ namespace string
 instance : inhabited string :=
 ⟨empty⟩
 
+instance : has_sizeof string :=
+⟨list.sizeof⟩
+
 @[pattern] def str : char → string → string := list.cons
 
 def concat (a b : string) : string :=