Documentation

Lean.Meta.Tactic.Simp.BuiltinSimprocs.Core

source
def reduceIte :
Lean.Meta.Simp.Simproc
Equations
    Instances For
      source
      def reduceDIte :
      Lean.Meta.Simp.Simproc
      Equations
        Instances For
          source
          def dreduceIte :
          Lean.Meta.Simp.DSimproc
          Equations
            Instances For
              source
              def dreduceDIte :
              Lean.Meta.Simp.DSimproc
              Equations
                Instances For
                  source
                  def reduceCtorEq :
                  Lean.Meta.Simp.Simproc
                  Equations
                    Instances For