Documentation

Lean.Meta.Tactic.Grind.Intro

Introduce new hypotheses (and apply by_contra) until goal is of the form ... ⊢ False or is inconsistent.

Equations
    Instances For

      Similar to intros, but returns true if new hypotheses have been added, and false otherwise.

      Equations
        Instances For
          def Lean.Meta.Grind.assertAt (proof prop : Expr) (generation : Nat) :

          Asserts a new fact prop with proof proof to the given goal.

          Equations
            Instances For

              Asserts next fact in the goal fact queue. Returns true if the queue was not empty and false otherwise.

              Equations
                Instances For

                  Asserts all facts in the goal fact queue. Returns true if the queue was not empty and false otherwise.

                  Equations
                    Instances For