def Lean.Meta.Grind.preprocessHypothesis (e : Expr) : GoalM Simp.Result

Similar to Grind.preprocess, but does not simplify e if isMatchCondCandidate (aka Simp.isEqnThmHypothesis) is true. We added this feature because it may be coming from external sources (e.g., manually applying an function induction principle before invoking grind).

Equations

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

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