From a0ed2d17388fdb50a10d170e84e9b6c4496cd7c1 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Wed, 27 Jan 2021 15:17:51 -0800
Subject: [PATCH] chore: update tests

---
 tests/playground/sizeof1.lean | 14 --------------
 tests/playground/sizeof2.lean | 10 ----------
 tests/playground/sizeof3.lean | 10 ----------
 3 files changed, 34 deletions(-)

diff --git a/tests/playground/sizeof1.lean b/tests/playground/sizeof1.lean
index 394c8fec68..f58c4b7ee3 100644
--- a/tests/playground/sizeof1.lean
+++ b/tests/playground/sizeof1.lean
@@ -47,17 +47,3 @@ theorem aux_4 [SizeOf α] [SizeOf β] (cs : List (List (TreeNeg α β))) : TreeP
       rw aux_3
       rfl)
     cs
-
-theorem TreePos.leaf.sizeOf_spec [SizeOf α] [SizeOf β] (a : α) : sizeOf (TreePos.leaf (β := β) a) = 1 + sizeOf a :=
-  rfl
-
-theorem TreePos.node.sizeOf_spec [SizeOf α] [SizeOf β] (cs : List (List (TreeNeg α β))) : sizeOf (TreePos.node cs) = 1 + sizeOf cs := by
-  show 1 + TreePos._sizeOf_3 cs = 1 + sizeOf cs
-  rw aux_4
-
-theorem TreeNeg.leaf.sizeOf_spec [SizeOf α] [SizeOf β] (b : β) : sizeOf (TreeNeg.leaf (α := α) b) = 1 + sizeOf b :=
-  rfl
-
-theorem TreeNeg.node.sizeOf_spec [SizeOf α] [SizeOf β] (cs : List (List (TreePos α β))) : sizeOf (TreeNeg.node cs) = 1 + sizeOf cs := by
-  show 1 + TreePos._sizeOf_4 cs = 1 + sizeOf cs
-  rw aux_2
diff --git a/tests/playground/sizeof2.lean b/tests/playground/sizeof2.lean
index 5272699a52..b4368ff483 100644
--- a/tests/playground/sizeof2.lean
+++ b/tests/playground/sizeof2.lean
@@ -16,13 +16,3 @@ theorem aux_1 [SizeOf α] (a : List (Arg α)) : Arg._sizeOf_3 a = sizeOf a := by
     show 1 + Arg._sizeOf_1 h + Arg._sizeOf_3 t = sizeOf (h :: t)
     rw ih
     rfl
-
-theorem Arg.val.sizeOf_spec [SizeOf α] (a : α) : sizeOf (Arg.val a) = 1 + sizeOf a :=
-  rfl
-
-theorem Arg.expr.sizeOf_spec [SizeOf α] (e : Expr α) : sizeOf (Arg.expr e) = 1 + sizeOf e :=
-  rfl
-
-theorem Expr.app.sizeOf_spec [SizeOf α] (f : String) (args : List (Arg α)) : sizeOf (Expr.app f args) = 1 + sizeOf f + sizeOf args := by
-  show 1 + sizeOf f + Arg._sizeOf_3 args = 1 + sizeOf f + sizeOf args
-  rw aux_1
diff --git a/tests/playground/sizeof3.lean b/tests/playground/sizeof3.lean
index cc5c192664..a225f31920 100644
--- a/tests/playground/sizeof3.lean
+++ b/tests/playground/sizeof3.lean
@@ -47,13 +47,3 @@ theorem aux_2 [SizeOf α] (a : BList (Foo α) (Boo α)) : Foo._sizeOf_4 a = size
       rw ih
       rfl)
     a
-
-end Foo
-
-theorem Foo.mk.sizeOf_spec [SizeOf α] (cs : AList (Foo α) (Boo α)) : sizeOf (Foo.mk cs) = 1 + sizeOf cs := by
-  show 1 + Foo._sizeOf_3 cs = 1 + sizeOf cs
-  rw Foo.aux_1
-
-theorem Boo.mk.sizeOf_spec [SizeOf α] (a : α) (cs : BList (Foo α) (Boo α)) : sizeOf (Boo.mk a cs) = 1 + sizeOf a + sizeOf cs := by
-  show 1 + sizeOf a + Foo._sizeOf_4 cs = 1 + sizeOf a + sizeOf cs
-  rw Foo.aux_2