Documentation

Lean.Compiler.LCNF.Simp.SimpValue

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

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

Equations
    Instances For
      source
      def Lean.Compiler.LCNF.Simp.simpAppApp? (e : LetValue) :
      OptionT SimpM 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 : LetValue) :
          OptionT SimpM LetValue
          Equations
            Instances For
              source
              def Lean.Compiler.LCNF.Simp.applyImplementedBy? (e : LetValue) :
              OptionT SimpM LetValue
              Equations
                Instances For
                  source
                  def Lean.Compiler.LCNF.Simp.simpValue? (e : LetValue) :
                  SimpM (Option LetValue)

                  Try to apply simple simplifications.

                  Equations
                    Instances For