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

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

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

@@ -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());
-}
-}

src/library/aux_recursors.h

@@ -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);
-}

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 {