Documentation

Lean.Compiler.LCNF.Simp

source
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.
source
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.
source
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
source
def Lean.Compiler.LCNF.simp (config : optParam Lean.Compiler.LCNF.Simp.Config { etaPoly := false, inlinePartial := false, implementedBy := false }) (occurrence : optParam Nat 0) :
Lean.Compiler.LCNF.Pass
Equations
  • One or more equations did not get rendered due to their size.