From 443615f27e53a0fa96a3d09b1d2f3f72fbf7f003 Mon Sep 17 00:00:00 2001
From: Sebastian Ullrich <sebasti@nullri.ch>
Date: Thu, 7 May 2026 13:18:33 +0200
Subject: [PATCH] test: remove `printDecls` test (#13677)

This is a test from the very beginnings of the elab framework, which has
since become the second-slowest test.
---
 tests/elab/printDecls.lean             | 26 --------------------------
 tests/elab/printDecls.lean.out.ignored |  0
 2 files changed, 26 deletions(-)
 delete mode 100644 tests/elab/printDecls.lean
 delete mode 100644 tests/elab/printDecls.lean.out.ignored

diff --git a/tests/elab/printDecls.lean b/tests/elab/printDecls.lean
deleted file mode 100644
index 6006ce421f..0000000000
--- a/tests/elab/printDecls.lean
+++ /dev/null
@@ -1,26 +0,0 @@
-import Lean
-
-open Lean
-open Lean.Meta
-
--- Return true if `declName` should be ignored
-def shouldIgnore (declName : Name) : Bool :=
-  declName.isInternal
-  || match declName with
-     | .str _ s => "match_".isPrefixOf s || "proof_".isPrefixOf s || "eq_".isPrefixOf s
-     | _ => true
-
--- Print declarations that have the given prefix.
-def printDecls (pre : Name) : MetaM Unit := do
-  let cs := (← getEnv).constants
-  cs.forM fun declName info => do
-    if pre.isPrefixOf declName && !shouldIgnore declName then
-      if let some docString ← findDocString? (← getEnv) declName then
-        IO.println s!"/-- {docString} -/\n{declName} : {← ppExpr info.type}"
-      else
-        IO.println s!"{declName} : {← ppExpr info.type}"
-
-#eval printDecls `Array
-#eval printDecls `List
-#eval printDecls `Bool
-#eval printDecls `Lean.Elab
diff --git a/tests/elab/printDecls.lean.out.ignored b/tests/elab/printDecls.lean.out.ignored
deleted file mode 100644
index e69de29bb2..0000000000