fix: shouldGenerateCode fix for axiom

src/Lean/Compiler/LCNF/Main.lean

@@ -27,7 +27,8 @@ and `[specialize]` since they can be partially applied.
 -/
 def shouldGenerateCode (declName : Name) : CoreM Bool := do
   if (← isCompIrrelevant |>.run') then return false
-  unless (← getConstInfo declName).hasValue do return false
+  let some info ← getDeclInfo? declName | return false
+  unless info.hasValue do return false
   let env ← getEnv
   if hasMacroInlineAttribute env declName then return false
   if (← Meta.isMatcher declName) then return false

src/Lean/Compiler/LCNF/ToDecl.lean

@@ -74,6 +74,15 @@ private def replaceUnsafeRecNames (value : Expr) : CoreM Expr :=
         return .done e
     | _ => return .continue
 
+/--
+Return the declaration `ConstantInfo` for the code generator.
+
+Remark: the unsafe recursive version is tried first.
+-/
+def getDeclInfo? (declName : Name) : CoreM (Option ConstantInfo) := do
+  let env ← getEnv
+  return env.find? (mkUnsafeRecName declName) <|> env.find? declName
+
 /--
 Convert the given declaration from the Lean environment into `Decl`.
 The steps for this are roughly:
@@ -84,8 +93,7 @@ The steps for this are roughly:
 - turn the resulting term into LCNF declaration
 -/
 def toDecl (declName : Name) : CompilerM Decl := do
-  let env ← getEnv
-  let some info := env.find? (mkUnsafeRecName declName) <|> env.find? declName | throwError "declaration `{declName}` not found"
+  let some info ← getDeclInfo? declName | throwError "declaration `{declName}` not found"
   let some value := info.value? | throwError "declaration `{declName}` does not have a value"
   let (type, value) ← Meta.MetaM.run' do
     let type  ← toLCNFType info.type

src/Lean/Compiler/LCNF/Util.lean

@@ -8,7 +8,6 @@ import Lean.MonadEnv
 import Lean.Util.Recognizers
 
 namespace Lean.Compiler.LCNF
-
 /--
 Return `true` if `mdata` should be preserved.
 Right now, we don't preserve any `MData`, but this may