Documentation

Lean.Meta.Tactic.Grind.Simp

Similar to simpCore, but uses dsimp.

Equations
    Instances For

      Preprocesses e using grind normalization theorems and simprocs, and then applies several other preprocessing steps.

      Equations
        Instances For
          def Lean.Meta.Grind.pushNewFact' (prop proof : Expr) (generation : Nat := 0) :
          Equations
            Instances For
              def Lean.Meta.Grind.pushNewFact (proof : Expr) (generation : Nat := 0) :

              Infers the type of the proof, preprocess it, and adds it to todo list.

              Equations
                Instances For