def Lean.Meta.Grind.propagateBeta (lams fns : Array Expr) : GoalM Unit

Tries to apply beta-reduction using the parent applications of the functions in fns with the lambda expressions in lams.

def Lean.Meta.Grind.addNewEq (lhs rhs proof : Expr) (generation : Nat) : GoalM Unit

Internalizes lhs and rhs, and then adds equality lhs = rhs.

def Lean.Meta.Grind.add (fact proof : Expr) (generation : Nat := 0) : GoalM Unit

Adds a new fact justified by the given proof and using the given generation.

def Lean.Meta.Grind.addHypothesis (fvarId : FVarId) (generation : Nat := 0) : GoalM Unit

Adds a new hypothesis.