Documentation

Lean.Compiler.LCNF.Simp.SimpValue

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

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

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

    Application over application.

    let g := f a
g b

    is simplified to f a b.

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

          Try to apply simple simplifications.

          Instances For