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

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

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

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

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.

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.