From 613c8027d7d741b7ff2817395513e5ca41dc7762 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Sun, 9 Oct 2022 11:49:11 -0700 Subject: [PATCH] fix: missing `instantiateParamsLevelParams` --- src/Lean/Compiler/LCNF/Simp/InlineProj.lean | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/src/Lean/Compiler/LCNF/Simp/InlineProj.lean b/src/Lean/Compiler/LCNF/Simp/InlineProj.lean index 4a04a6ba68..248a2cb40c 100644 --- a/src/Lean/Compiler/LCNF/Simp/InlineProj.lean +++ b/src/Lean/Compiler/LCNF/Simp/InlineProj.lean @@ -63,8 +63,9 @@ where let .const declName us := e.getAppFn | failure let some decl ← getDecl? declName | failure guard (decl.getArity == e.getAppNumArgs) + let params := decl.instantiateParamsLevelParams us let code := decl.instantiateValueLevelParams us - let code ← betaReduce decl.params code e.getAppArgs (mustInline := true) + let code ← betaReduce params code e.getAppArgs (mustInline := true) visitCode code projs visitCode (code : Code) (projs : List Nat) : OptionT (StateRefT (Array CodeDecl) SimpM) FVarId := do