def Lean.Meta.Grind.Goal.lastDecl? (goal : Goal) : MetaM (Option LocalDecl)

Equations

• goal.lastDecl? = do let __do_lift ← goal.mvarId.getDecl pure __do_lift.lctx.lastDecl

def Lean.Meta.Grind.Action.intro (generation : Nat) : Action

Equations

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

def Lean.Meta.Grind.Action.intros (generation : Nat) : Action

Equations

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

def Lean.Meta.Grind.Action.assertNext : Action

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.Action.assertAll : Action

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

Equations

• Lean.Meta.Grind.Action.assertAll = Lean.Meta.Grind.Action.loop Lean.Meta.Grind.Action.hugeNumber✝ Lean.Meta.Grind.Action.assertNext

------------------------------------------ ------------------------------------------ TODO Delete rest of the file ------------------------------------------ ------------------------------------------

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.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.