source
partial def Lean.IR.pushProjs (bs : Array FnBody) (alts : Array Alt) (altsF : Array IndexSet) (ctx : Array FnBody) (ctxF : IndexSet) :
Array FnBody × Array Alt
source
partial def Lean.IR.FnBody.pushProj (b : FnBody) :
FnBody
source
def Lean.IR.Decl.pushProj (d : Decl) :
Decl

Push projections inside `case` branches.

Equations

- (Lean.IR.Decl.fdecl f xs type b info).pushProj = ((Lean.IR.Decl.fdecl f xs type b info).updateBody! b.pushProj).normalizeIds
- d.pushProj = d

Instances For