Documentation

Lean.Compiler.IR.SimpCase

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

Array Lean.IR.Alt

Equations

Lean.IR.ensureHasDefault alts = if Array.any alts Lean.IR.Alt.isDefault 0 (Array.size alts) = true then alts else if Array.size alts < 2 then alts else let last := Array.back alts; let alts := Array.pop alts; Array.push alts (Lean.IR.Alt.default (Lean.IR.AltCore.body last))

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

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

Equations

Lean.IR.Decl.simpCase d = match d with | Lean.IR.Decl.fdecl x x_1 x_2 b x_3 => Lean.IR.Decl.updateBody! d (Lean.IR.FnBody.simpCase b) | other => other