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 : Lean.Meta.Grind.Goal) (generation : Nat) : Lean.Meta.Grind.GrindM (List Lean.Meta.Grind.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 : Lean.Meta.Grind.Goal) : StateRefT' IO.RealWorld (Array Lean.Meta.Grind.Goal) Lean.Meta.Grind.GrindM Unit

def Lean.Meta.Grind.assertAt (goal : Lean.Meta.Grind.Goal) (proof prop : Lean.Expr) (generation : Nat) : Lean.Meta.Grind.GrindM (List Lean.Meta.Grind.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 : Lean.Meta.Grind.Goal) : Lean.Meta.Grind.GrindM (Option (List Lean.Meta.Grind.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 : Lean.Meta.Grind.Goal) (f : Lean.Meta.Grind.Goal → Lean.Meta.Grind.GrindM (Option (List Lean.Meta.Grind.Goal))) : Lean.Meta.Grind.GrindM (List Lean.Meta.Grind.Goal)

Equations

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

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

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

Asserts all facts in the goal fact queue.

Equations

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