def reduceBEq : Lean.Meta.Simp.Simproc

This simproc reduces _ == _ when both arguments are constructor applications and the BEq instance in question has been annotated with @[method_specs].

def reduceOrd : Lean.Meta.Simp.Simproc

This simproc reduces Ord.compare _ _ when both arguments are constructor applications and the Ord instance in question has been annotated with @[method_specs].