Documentation

Lean.Compiler.IR.SimpCase

source
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.
Instances For
    source
    partial def Lean.IR.FnBody.simpCase (b : Lean.IR.FnBody) :
    Lean.IR.FnBody
    source
    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
    • d.simpCase = match d with | Lean.IR.Decl.fdecl f xs type b info => d.updateBody! b.simpCase | other => other
    Instances For