From 5814c1e757ced7d55e047edd062c1b9e155ae782 Mon Sep 17 00:00:00 2001
From: Cameron Zwarich <cameron@lean-fro.org>
Date: Wed, 28 May 2025 13:56:03 -0700
Subject: [PATCH] fix: recursively process jmp args in LCNF.toMono (#8521)

This PR makes LCNF.toMono recursively process jmp args.
---
 src/Lean/Compiler/LCNF/ToMono.lean | 3 ++-
 1 file changed, 2 insertions(+), 1 deletion(-)

diff --git a/src/Lean/Compiler/LCNF/ToMono.lean b/src/Lean/Compiler/LCNF/ToMono.lean
index 55687d82a2..e5a2a793e5 100644
--- a/src/Lean/Compiler/LCNF/ToMono.lean
+++ b/src/Lean/Compiler/LCNF/ToMono.lean
@@ -221,7 +221,8 @@ partial def Code.toMono (code : Code) : ToMonoM Code := do
   | .let decl k => return code.updateLet! (← decl.toMono) (← k.toMono)
   | .fun decl k | .jp decl k => return code.updateFun! (← decl.toMono) (← k.toMono)
   | .unreach type => return .unreach (← toMonoType type)
-  | .return .. | .jmp .. => return code
+  | .jmp fvarId args => return code.updateJmp! fvarId (← args.mapM argToMono)
+  | .return .. => return code
   | .cases c =>
     if h : c.typeName == ``Decidable then
       decToMono c h