From f236328bc3744d23685defa9c1ad69263ca26cb9 Mon Sep 17 00:00:00 2001 From: Cameron Zwarich Date: Mon, 4 Aug 2025 19:41:36 -0700 Subject: [PATCH] chore: don't check type of erased arguments in FixedParams analysis (#9602) --- src/Lean/Compiler/LCNF/FixedParams.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/Lean/Compiler/LCNF/FixedParams.lean b/src/Lean/Compiler/LCNF/FixedParams.lean index f0b5db4b70..717e8266c4 100644 --- a/src/Lean/Compiler/LCNF/FixedParams.lean +++ b/src/Lean/Compiler/LCNF/FixedParams.lean @@ -145,7 +145,7 @@ partial def evalApp (declName : Name) (args : Array Arg) : FixParamM Unit := do have : i < main.params.size := h.2 let param := main.params[i] let val ← evalArg args[i] - unless val == .val i || (val == .erased && param.type.isErased) do + unless val == .val i || val == .erased do -- Found non fixed argument -- Remark: if the argument is erased and the type of the parameter is erased we assume it is a fixed "propositonal" parameter. modify fun s => { s with fixed := s.fixed.set! i false }