From d6ba0592d175bbe553cff7d590ed2196757adeaf Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Sun, 13 Dec 2020 15:50:08 -0800 Subject: [PATCH] chore: remove dead code --- tests/playground/deriving.lean | 8 -------- 1 file changed, 8 deletions(-) diff --git a/tests/playground/deriving.lean b/tests/playground/deriving.lean index a40271ad5d..1b32a8971f 100644 --- a/tests/playground/deriving.lean +++ b/tests/playground/deriving.lean @@ -99,14 +99,6 @@ namespace Deriving /- For type classes such as BEq, ToString, Format -/ namespace Default -structure AuxFun where - name : Name - declSig : Array Syntax := #[] - type : Syntax := Syntax.missing - value : Syntax := Syntax.missing - -structure State where - auxFns : NameMap AuxFun -- type name to function structure ContextCore where classInfo : ConstantInfo