From cf13b29760aa65642e2e3a4eebd0cfcc883ea9f2 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Sun, 6 Nov 2022 18:14:23 -0800 Subject: [PATCH] fix: nasty bug due to #1804 --- src/Lean/Compiler/LCNF/ReduceArity.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/Lean/Compiler/LCNF/ReduceArity.lean b/src/Lean/Compiler/LCNF/ReduceArity.lean index eb443d0bf1..26ee53469a 100644 --- a/src/Lean/Compiler/LCNF/ReduceArity.lean +++ b/src/Lean/Compiler/LCNF/ReduceArity.lean @@ -124,7 +124,7 @@ abbrev ReduceM := ReaderT Context CompilerM partial def reduce (code : Code) : ReduceM Code := do match code with | .let decl k => - let .const declName _ args := decl.value | return code.updateLet! decl (← reduce k) + let .const declName _ args := decl.value | do return code.updateLet! decl (← reduce k) unless declName == (← read).declName do return code.updateLet! decl (← reduce k) let mut argsNew := #[] for used in (← read).paramMask, arg in args do