def Lean.Compiler.LCNF.Decl.simp? (decl : Lean.Compiler.LCNF.Decl) : Lean.Compiler.LCNF.Simp.SimpM (Option Lean.Compiler.LCNF.Decl)

Equations

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

def Lean.Compiler.LCNF.Decl.simp (decl : Lean.Compiler.LCNF.Decl) (config : Lean.Compiler.LCNF.Simp.Config) : Lean.Compiler.LCNF.CompilerM Lean.Compiler.LCNF.Decl

Equations

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

partial def Lean.Compiler.LCNF.Decl.simp.go (decl : Lean.Compiler.LCNF.Decl) (config : Lean.Compiler.LCNF.Simp.Config) : Lean.Compiler.LCNF.CompilerM Lean.Compiler.LCNF.Decl

def Lean.Compiler.LCNF.simp (config : optParam Lean.Compiler.LCNF.Simp.Config { etaPoly := false, inlinePartial := false, implementedBy := false, inlineDefs := true }) (occurrence : optParam Nat 0) (phase : optParam Lean.Compiler.LCNF.Phase Lean.Compiler.LCNF.Phase.base) : Lean.Compiler.LCNF.Pass

Equations

• Lean.Compiler.LCNF.simp config occurrence phase = Lean.Compiler.LCNF.Pass.mkPerDeclaration `simp (fun x => Lean.Compiler.LCNF.Decl.simp x config) phase occurrence