From bebce084fad817d38b7249054dcedcf2d4972520 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Sun, 16 Oct 2022 07:38:40 -0700 Subject: [PATCH] fix: bug at `toLCNF.visitMData` --- src/Lean/Compiler/LCNF/ToLCNF.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/Lean/Compiler/LCNF/ToLCNF.lean b/src/Lean/Compiler/LCNF/ToLCNF.lean index 84f78e080a..cd13425a9c 100644 --- a/src/Lean/Compiler/LCNF/ToLCNF.lean +++ b/src/Lean/Compiler/LCNF/ToLCNF.lean @@ -714,7 +714,7 @@ where return .fvar funDecl.fvarId visitMData (mdata : MData) (e : Expr) : M Expr := do - if let some (.app (.lam n t b ..) v) := letFunAnnotation? e then + if let some (.app (.lam n t b ..) v) := letFunAnnotation? (.mdata mdata e) then visitLet (.letE n t v b (nonDep := true)) #[] else if isCompilerRelevantMData mdata then mkAuxLetDecl <| .mdata mdata (← visit e)