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