Documentation

Lean.Compiler.LCNF.Simp

source
def Lean.Compiler.LCNF.Decl.simp? (decl : Decl Purity.pure) :
Simp.SimpM (Option (Decl Purity.pure))
Equations
  • One or more equations did not get rendered due to their size.
Instances For
    source
    def Lean.Compiler.LCNF.Decl.simp (decl : Decl Purity.pure) (config : Simp.Config) :
    CompilerM (Decl Purity.pure)
    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
      source
      def Lean.Compiler.LCNF.simp (config : Simp.Config := { }) (occurrence : Nat := 0) (phase : Phase := Phase.base) :
      Pass
      Equations
      • One or more equations did not get rendered due to their size.
      Instances For