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

Equations

• reduceBEq e = if e.isAppOfArity `BEq.beq 4 = true then reduceMethod✝ "beq" e else pure Lean.Meta.Simp.Step.continue

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

Equations

• reduceOrd e = if e.isAppOfArity `Ord.compare 4 = true then reduceMethod✝ "compare" e else pure Lean.Meta.Simp.Step.continue