Documentation

Lean.Meta.Tactic.Grind.Core

source
def Lean.Meta.Grind.addEq (lhs rhs proof : Lean.Expr) :
Lean.Meta.Grind.GoalM Unit
Equations
Instances For
    source
    def Lean.Meta.Grind.addHEq (lhs rhs proof : Lean.Expr) :
    Lean.Meta.Grind.GoalM Unit
    Equations
    Instances For
      source
      def Lean.Meta.Grind.add (fact proof : Lean.Expr) (generation : Nat := 0) :
      Lean.Meta.Grind.GoalM Unit

      Adds a new fact justified by the given proof and using the given generation.

      Equations
      • One or more equations did not get rendered due to their size.
      Instances For
        source
        def Lean.Meta.Grind.add.go (proof : Lean.Expr) (generation : Nat := 0) (p : Lean.Expr) (isNeg : Bool) :
        Lean.Meta.Grind.GoalM Unit
        Equations
        • One or more equations did not get rendered due to their size.
        Instances For
          source
          def Lean.Meta.Grind.add.goEq (proof : Lean.Expr) (generation : Nat := 0) (p lhs rhs : Lean.Expr) (isNeg isHEq : Bool) :
          Lean.Meta.Grind.GoalM Unit
          Equations
          • One or more equations did not get rendered due to their size.
          Instances For
            source
            def Lean.Meta.Grind.addHypothesis (fvarId : Lean.FVarId) (generation : Nat := 0) :
            Lean.Meta.Grind.GoalM Unit

            Adds a new hypothesis.

            Equations
            Instances For