chore(library/init/lean/compiler): modifiedJPVals ==> modifyJPs
This commit is contained in:
parent
2c4811a808
commit
805ee81e73
4 changed files with 4 additions and 4 deletions
|
|
@ -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
|
||||
|
|
|
|||
|
|
@ -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
|
||||
|
|
|
|||
|
|
@ -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
|
||||
|
|
|
|||
|
|
@ -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
|
||||
|
|
|
|||
Loading…
Add table
Reference in a new issue