Documentation

Lean.Meta.Tactic.Simp.BuiltinSimprocs.Core

source
def reduceIte :
Lean.Meta.Simp.Simproc
Equations
  • One or more equations did not get rendered due to their size.
Instances For
    source
    def reduceDIte :
    Lean.Meta.Simp.Simproc
    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
      source
      def dreduceIte :
      Lean.Meta.Simp.DSimproc
      Equations
      • One or more equations did not get rendered due to their size.
      Instances For
        source
        def dreduceDIte :
        Lean.Meta.Simp.DSimproc
        Equations
        • One or more equations did not get rendered due to their size.
        Instances For
          source
          def reduceCtorEq :
          Lean.Meta.Simp.Simproc
          Equations
          • One or more equations did not get rendered due to their size.
          Instances For