partial def Lean.IR.pushProjs (bs : Array Lean.IR.FnBody) (alts : Array Lean.IR.Alt) (altsF : Array Lean.IR.IndexSet) (ctx : Array Lean.IR.FnBody) (ctxF : Lean.IR.IndexSet) : Array Lean.IR.FnBody × Array Lean.IR.Alt

partial def Lean.IR.FnBody.pushProj (b : Lean.IR.FnBody) : Lean.IR.FnBody

def Lean.IR.Decl.pushProj (d : Lean.IR.Decl) : Lean.IR.Decl

Push projections inside case branches.

Equations

• Lean.IR.Decl.pushProj d = match d with | Lean.IR.Decl.fdecl f xs type b info => Lean.IR.Decl.normalizeIds (Lean.IR.Decl.updateBody! d (Lean.IR.FnBody.pushProj b)) | other => other