source
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

Instances For

source
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

Instances For