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.

def Lean.Meta.Grind.isMorallyIff (e : Expr) : Bool

Returns true if e is of the form @Eq Prop a b

Equations

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

def Lean.Meta.Grind.activateTheorem (thm : EMatchTheorem) (generation : Nat) : GoalM Unit

Equations

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