perf: do not consult isNoConfusion in whnf (#11571)

This PR lets `whnf` not consult `isNoConfusion`, to speed up this hot
path a bit.

Author: nomeata

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
 

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`.

src/library/CMakeLists.txt

@@ -3,7 +3,6 @@ add_library(library OBJECT expr_lt.cpp
   module.cpp dynlib.cpp replace_visitor.cpp num.cpp
   class.cpp util.cpp print.cpp annotation.cpp
   reducible.cpp init_module.cpp
-  aux_recursors.cpp
   profiling.cpp time_task.cpp
   formatter.cpp
   elab_environment.cpp

src/library/aux_recursors.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 {