def Lean.IR.ensureHasDefault (alts : Array Lean.IR.Alt) : Array Lean.IR.Alt

Equations

• One or more equations did not get rendered due to their size.

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

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

Simplify case

• Remove unreachable branches.
• Remove case if there is only one branch.
• Merge most common branches using Alt.default.

Equations

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