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

Equations

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

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

Equations

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

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

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

Equations

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