Support for type class `LawfulEqCmp`.

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

Instances For

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

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

Instances For