Documentation

Lean.Compiler.LCNF.Simp.SimpValue

source
def Lean.Compiler.LCNF.Simp.simpProj? (e : Lean.Compiler.LCNF.LetValue) :
OptionT Lean.Compiler.LCNF.Simp.SimpM Lean.Compiler.LCNF.LetValue

Try to simplify projections .proj _ i s where s is constructor.

Equations
Instances For
    source
    def Lean.Compiler.LCNF.Simp.simpAppApp? (e : Lean.Compiler.LCNF.LetValue) :
    OptionT Lean.Compiler.LCNF.Simp.SimpM Lean.Compiler.LCNF.LetValue

    Application over application.

    let g := f a
g b

    is simplified to f a b.

    Equations
    Instances For
      source
      def Lean.Compiler.LCNF.Simp.simpCtorDiscr? (e : Lean.Compiler.LCNF.LetValue) :
      OptionT Lean.Compiler.LCNF.Simp.SimpM Lean.Compiler.LCNF.LetValue
      Instances For
        source
        def Lean.Compiler.LCNF.Simp.applyImplementedBy? (e : Lean.Compiler.LCNF.LetValue) :
        OptionT Lean.Compiler.LCNF.Simp.SimpM Lean.Compiler.LCNF.LetValue
        Instances For
          source
          def Lean.Compiler.LCNF.Simp.simpValue? (e : Lean.Compiler.LCNF.LetValue) :
          Lean.Compiler.LCNF.Simp.SimpM (Option Lean.Compiler.LCNF.LetValue)

          Try to apply simple simplifications.

          Instances For