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 (goal : Goal) (generation : Nat) : GrindM (List Goal)

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

Equations

• Lean.Meta.Grind.intros goal generation = 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 (goal : Goal) (proof prop : Expr) (generation : Nat) : GrindM (List Goal)

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? (goal : Goal) : GrindM (Option (List Goal))

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.iterate (goal : Goal) (f : Goal → GrindM (Option (List Goal))) : GrindM (List Goal)

Equations

• Lean.Meta.Grind.iterate goal f = Lean.Meta.Grind.iterate.go f [goal] []

partial def Lean.Meta.Grind.iterate.go (f : Goal → GrindM (Option (List Goal))) (todo result : List Goal) : GrindM (List Goal)

def Lean.Meta.Grind.assertAll (goal : Goal) : GrindM (List Goal)

Asserts all facts in the goal fact queue.

Equations

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