From 11a332999215b730eed3b54f3b90bf29ce122c6c Mon Sep 17 00:00:00 2001
From: Joachim Breitner <mail@joachim-breitner.de>
Date: Tue, 9 Dec 2025 21:53:40 +0000
Subject: [PATCH 1/2] perf: do not consult isNoConfusion in whnf

---
 src/Lean/AuxRecursor.lean              |  2 --
 src/Lean/Meta/WHNF.lean                |  2 +-
 src/library/CMakeLists.txt             |  1 -
 src/library/aux_recursors.cpp          | 20 --------------------
 src/library/aux_recursors.h            | 15 ---------------
 src/library/constructions/cases_on.cpp |  1 -
 6 files changed, 1 insertion(+), 40 deletions(-)
 delete mode 100644 src/library/aux_recursors.cpp
 delete mode 100644 src/library/aux_recursors.h

diff --git a/src/Lean/AuxRecursor.lean b/src/Lean/AuxRecursor.lean
index 4bad8afc7e07..1e0d6f075ca0 100644
--- a/src/Lean/AuxRecursor.lean
+++ b/src/Lean/AuxRecursor.lean
@@ -28,7 +28,6 @@ builtin_initialize auxRecExt : TagDeclarationExtension ← mkTagDeclarationExten
 def markAuxRecursor (env : Environment) (declName : Name) : Environment :=
   auxRecExt.tag env declName
 
-@[export lean_is_aux_recursor]
 def isAuxRecursor (env : Environment) (declName : Name) : Bool :=
   auxRecExt.isTagged env declName
   -- TODO: use `markAuxRecursor` when they are defined
@@ -68,7 +67,6 @@ builtin_initialize noConfusionExt : TagDeclarationExtension ← mkTagDeclaration
 def markNoConfusion (env : Environment) (n : Name) : Environment :=
   noConfusionExt.tag env n
 
-@[export lean_is_no_confusion]
 def isNoConfusion (env : Environment) (n : Name) : Bool :=
   noConfusionExt.isTagged env n
 
diff --git a/src/Lean/Meta/WHNF.lean b/src/Lean/Meta/WHNF.lean
index 015ed2994a19..809fbcc0b4ec 100644
--- a/src/Lean/Meta/WHNF.lean
+++ b/src/Lean/Meta/WHNF.lean
@@ -77,7 +77,7 @@ def smartUnfoldingMatchAlt? (e : Expr) : Option Expr :=
 
 def isAuxDef (constName : Name) : MetaM Bool := do
   let env ← getEnv
-  return isAuxRecursor env constName || isNoConfusion env constName
+  return isAuxRecursor env constName
 
 /--
 Retrieves `ConstInfo` for `declName`.
diff --git a/src/library/CMakeLists.txt b/src/library/CMakeLists.txt
index 0ae4d0dcdcb8..b0779630289d 100644
--- a/src/library/CMakeLists.txt
+++ b/src/library/CMakeLists.txt
@@ -4,7 +4,6 @@ add_library(library OBJECT expr_lt.cpp
   class.cpp util.cpp print.cpp annotation.cpp
   reducible.cpp init_module.cpp
   projection.cpp
-  aux_recursors.cpp
   profiling.cpp time_task.cpp
   formatter.cpp
   elab_environment.cpp
diff --git a/src/library/aux_recursors.cpp b/src/library/aux_recursors.cpp
deleted file mode 100644
index d4134090fb75..000000000000
--- a/src/library/aux_recursors.cpp
+++ /dev/null
@@ -1,20 +0,0 @@
-/*
-Copyright (c) 2015 Microsoft Corporation. All rights reserved.
-Released under Apache 2.0 license as described in the file LICENSE.
-
-Author: Leonardo de Moura
-*/
-#include "library/aux_recursors.h"
-
-namespace lean {
-extern "C" uint8 lean_is_aux_recursor(object * env, object * n);
-extern "C" uint8 lean_is_no_confusion(object * env, object * n);
-
-bool is_aux_recursor(elab_environment const & env, name const & r) {
-    return lean_is_aux_recursor(env.to_obj_arg(), r.to_obj_arg());
-}
-
-bool is_no_confusion(elab_environment const & env, name const & r) {
-    return lean_is_no_confusion(env.to_obj_arg(), r.to_obj_arg());
-}
-}
diff --git a/src/library/aux_recursors.h b/src/library/aux_recursors.h
deleted file mode 100644
index 1d66ee423ff7..000000000000
--- a/src/library/aux_recursors.h
+++ /dev/null
@@ -1,15 +0,0 @@
-/*
-Copyright (c) 2015 Microsoft Corporation. All rights reserved.
-Released under Apache 2.0 license as described in the file LICENSE.
-
-Author: Leonardo de Moura
-*/
-#pragma once
-#include "library/elab_environment.h"
-
-namespace lean {
-/** \brief Return true iff \c n is the name of an auxiliary recursor.
-    \see add_aux_recursor */
-bool is_aux_recursor(elab_environment const & env, name const & n);
-bool is_no_confusion(elab_environment const & env, name const & n);
-}
diff --git a/src/library/constructions/cases_on.cpp b/src/library/constructions/cases_on.cpp
index c18d32a831be..90f24bfb1102 100644
--- a/src/library/constructions/cases_on.cpp
+++ b/src/library/constructions/cases_on.cpp
@@ -13,7 +13,6 @@ Author: Leonardo de Moura
 #include "library/suffixes.h"
 #include "library/reducible.h"
 #include "library/constants.h"
-#include "library/aux_recursors.h"
 #include "library/constructions/util.h"
 
 namespace lean {

From 0ca0ab4610be1637d17f475c5b71e024a1f2691f Mon Sep 17 00:00:00 2001
From: Joachim Breitner <mail@joachim-breitner.de>
Date: Tue, 9 Dec 2025 22:26:19 +0000
Subject: [PATCH 2/2] Kick CI