Support for type class LawfulEqCmp.

def Lean.Meta.Grind.getLawfulEqCmpThm? (op : Expr) : GrindM (Option Expr)

If op implements LawfulEqCmp, then returns the proof term for ∀ a b, op a b = .eq → a = b

Equations

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

def Lean.Meta.Grind.getLawfulEqCmpThm?.go? (op : Expr) : MetaM (Option Expr)

Equations

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

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

Equations

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