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

Equations

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

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

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

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

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

def Lean.Meta.Grind.assertAt (proof prop : Expr) (generation : Nat) : SearchM Unit

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 : SearchM Bool

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

Equations

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

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

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