Support for type class ReflCmp.

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

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

Equations

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

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

Equations

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

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

Equations

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