chore: update tests

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

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

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