Documentation

Lean.Meta.Tactic.Grind.Intro

source
instance Lean.Meta.Grind.instInhabitedIntroResult :
Inhabited Lean.Meta.Grind.IntroResult✝
Equations
    source
    def Lean.Meta.Grind.intros (generation : Nat) :
    SearchM Unit

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

    Equations
      Instances For
        source
        def Lean.Meta.Grind.intros' (generation : Nat) :
        SearchM Bool

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

        Equations
          Instances For
            source
            def Lean.Meta.Grind.assertNext :
            SearchM Bool

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

            Equations
              Instances For
                source
                def Lean.Meta.Grind.assertAll :
                SearchM Bool

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

                Equations
                  Instances For