From 623e8cddf6ee9a6bd19e2d2c6c0ca657bdfbb4af Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Sun, 6 Nov 2022 08:04:02 -0800 Subject: [PATCH] fix: `ReduceArity.lean` --- src/Lean/Compiler/LCNF/ReduceArity.lean | 4 +++- 1 file changed, 3 insertions(+), 1 deletion(-) diff --git a/src/Lean/Compiler/LCNF/ReduceArity.lean b/src/Lean/Compiler/LCNF/ReduceArity.lean index 3e27aecdb6..eb443d0bf1 100644 --- a/src/Lean/Compiler/LCNF/ReduceArity.lean +++ b/src/Lean/Compiler/LCNF/ReduceArity.lean @@ -80,7 +80,7 @@ def visitLetExpr (e : LetExpr) : FindUsedM Unit := do | .fvar fvarId => unless fvarId == param.fvarId do visitFVar fvarId - | .erased | .type .. => return () + | .erased | .type .. => pure () -- over-application for arg in args[decl.params.size:] do visitArg arg @@ -88,6 +88,8 @@ def visitLetExpr (e : LetExpr) : FindUsedM Unit := do for param in decl.params[args.size:] do -- If recursive function is partially applied, we assume missing parameters are used because we don't want to eta-expand. visitFVar param.fvarId + else + args.forM visitArg partial def visit (code : Code) : FindUsedM Unit := do match code with