Documentation

Lean.Meta.Tactic.Grind.Simp

Similar to simpCore, but uses dsimp.

Equations
  • One or more equations did not get rendered due to their size.
Instances For

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

    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
      def Lean.Meta.Grind.pushNewFact' (prop proof : Expr) (generation : Nat := 0) :
      Equations
      • One or more equations did not get rendered due to their size.
      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
        • One or more equations did not get rendered due to their size.
        Instances For