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 do let y ← pure PUnit.unit (fun (y : PUnit) => reduceMethod✝ "beq" e) y 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 do let y ← pure PUnit.unit (fun (y : PUnit) => reduceMethod✝ "compare" e) y else pure Lean.Meta.Simp.Step.continue