source
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

Instances For

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

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

Instances For

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

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

Instances For

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

Instances For

source
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

Instances For

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

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

Instances For

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

Instances For

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

Instances For

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

Instances For