def Lean.Meta.Grind.addCongrTable (e : Expr) : GoalM Unit

Adds e to congruence table.

Equations

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

partial def Lean.Meta.Grind.internalize (e : Expr) (generation : Nat) : GoalM Unit