max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

fix: bug at toLCNF.visitMData

Browse source
This commit is contained in:
Leonardo de Moura 2022-10-16 07:38:40 -07:00
parent 8a81dfb876
commit bebce084fa
1 changed files with 1 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
src/Lean/Compiler/LCNF/ToLCNF.lean
View file

@ -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)