From 18b5ff9e78201b998c8a8e13bc2320e79c9eaa3a Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Fri, 30 Sep 2022 20:01:18 -0700
Subject: [PATCH] chore: propagate `recursive` flag during code specialization

---
 src/Lean/Compiler/LCNF/Specialize.lean | 3 ++-
 1 file changed, 2 insertions(+), 1 deletion(-)

diff --git a/src/Lean/Compiler/LCNF/Specialize.lean b/src/Lean/Compiler/LCNF/Specialize.lean
index 4be3e77fd0..0973ff9099 100644
--- a/src/Lean/Compiler/LCNF/Specialize.lean
+++ b/src/Lean/Compiler/LCNF/Specialize.lean
@@ -327,7 +327,8 @@ where
     let type ← value.inferType
     let type ← mkForallParams params type
     let safe := decl.safe
-    let decl := { name := nameNew, levelParams := levelParamsNew, params, type, value, safe : Decl }
+    let recursive := decl.recursive
+    let decl := { name := nameNew, levelParams := levelParamsNew, params, type, value, safe, recursive : Decl }
     return decl.setLevelParams
 
 /--