instance Lean.Meta.Grind.instInhabitedIntroResult : Inhabited Lean.Meta.Grind.IntroResult✝

Equations

• Lean.Meta.Grind.instInhabitedIntroResult = { default := Lean.Meta.Grind.IntroResult.done✝ }

def Lean.Meta.Grind.intros (generation : Nat) : GrindTactic'

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

Equations

• Lean.Meta.Grind.intros generation goal = do let __discr ← (Lean.Meta.Grind.intros.go generation goal).run #[] match __discr with | (fst, goals) => pure goals.toList

partial def Lean.Meta.Grind.intros.go (generation : Nat) (goal : Goal) : StateRefT' IO.RealWorld (Array Goal) GrindM Unit

def Lean.Meta.Grind.assertAt (proof prop : Expr) (generation : Nat) : GrindTactic'

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

Equations

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

def Lean.Meta.Grind.assertNext : GrindTactic

Asserts next fact in the goal fact queue.

Equations

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

def Lean.Meta.Grind.assertAll : GrindTactic

Asserts all facts in the goal fact queue.

Equations

• Lean.Meta.Grind.assertAll = Lean.Meta.Grind.assertNext.iterate