diff --git a/library/init/lean/compiler/elimdead.lean b/library/init/lean/compiler/elimdead.lean index 3461bb48d9..934c415fdf 100644 --- a/library/init/lean/compiler/elimdead.lean +++ b/library/init/lean/compiler/elimdead.lean @@ -32,7 +32,7 @@ reshapeWithoutDeadAux bs term term.freeVars partial def FnBody.elimDead : FnBody → FnBody | b := let (bs, term) := b.flatten in - let bs := modifyJPVals bs FnBody.elimDead in + let bs := modifyJPs bs FnBody.elimDead in let term := match term with | FnBody.case tid x alts := let alts := alts.hmap $ λ alt, alt.modifyBody FnBody.elimDead in diff --git a/library/init/lean/compiler/ir.lean b/library/init/lean/compiler/ir.lean index 0ee713c54b..569537757e 100644 --- a/library/init/lean/compiler/ir.lean +++ b/library/init/lean/compiler/ir.lean @@ -284,7 +284,7 @@ partial def reshapeAux : Array FnBody → Nat → FnBody → FnBody def reshape (bs : Array FnBody) (term : FnBody) : FnBody := reshapeAux bs bs.size term -@[inline] def modifyJPVals (bs : Array FnBody) (f : FnBody → FnBody) : Array FnBody := +@[inline] def modifyJPs (bs : Array FnBody) (f : FnBody → FnBody) : Array FnBody := bs.hmap $ λ b, match b with | FnBody.jdecl j xs t v k := FnBody.jdecl j xs t (f v) k | other := other diff --git a/library/init/lean/compiler/pushproj.lean b/library/init/lean/compiler/pushproj.lean index f2a9e51398..146d22bfcf 100644 --- a/library/init/lean/compiler/pushproj.lean +++ b/library/init/lean/compiler/pushproj.lean @@ -36,7 +36,7 @@ partial def pushProjs : Array FnBody → Array Alt → Array IndexSet → Array partial def FnBody.pushProj : FnBody → FnBody | b := let (bs, term) := b.flatten in - let bs := modifyJPVals bs FnBody.pushProj in + let bs := modifyJPs bs FnBody.pushProj in match term with | FnBody.case tid x alts := let afvs := alts.map $ λ alt, alt.body.freeVars in diff --git a/library/init/lean/compiler/simpcase.lean b/library/init/lean/compiler/simpcase.lean index f431073a23..5f4e44950b 100644 --- a/library/init/lean/compiler/simpcase.lean +++ b/library/init/lean/compiler/simpcase.lean @@ -37,7 +37,7 @@ else partial def FnBody.simpCase : FnBody → FnBody | b := let (bs, term) := b.flatten in - let bs := modifyJPVals bs FnBody.simpCase in + let bs := modifyJPs bs FnBody.simpCase in match term with | FnBody.case tid x alts := let alts := alts.hmap $ λ alt, alt.modifyBody FnBody.simpCase in