[Merged by Bors] - chore(Order.Grade): remove porting notes

[mattrobball]

Simple changes to remove porting notes.

---

[j-loreaux]

According to the note:

-- porting note - what the hell?! used to be grade 𝕆

it seems that grade should have an explicit argument, but in your code you just have grade, so it's implicit. Or am I missing something?

[mattrobball]

Yes. I guess we could try to change the binder type in grade to be explicit but this seemed ok otherwise.

[Ruben-VandeVelde]

According to the note:

-- porting note - what the hell?! used to be grade 𝕆

it seems that grade should have an explicit argument, but in your code you just have grade, so it's implicit. Or am I missing something?

What happened here is that GradeOrder.grade takes an implicit 𝕆 and _root_.grade takes an explicit 𝕆. Definitions in the GradeOrder namespace now pick GradeOrder.grade. We could use

class GradeOrder (𝕆 α : Type*) [Preorder 𝕆] [Preorder α] where
  /-- The grading function. -/
  protected grade : α → 𝕆

to avoid this

[mattrobball]

I used _root_.grade in those two locations.

Making it protected is sensible but out of scope for this PR. I would be happy if there is a separate one doing this.

[j-loreaux]

bors merge

[mattrobball]

Note: the first porting note was an instance of leanprover/lean4#2789

[mathlib-bors]

Build failed (retrying...):

• Build

[mathlib-bors]

Build failed (retrying...):

• Build

[mattrobball]

bors r-

[mathlib-bors]

Canceled.

[mattrobball]

bors merge

[mathlib-bors]

Pull request successfully merged into master.

Build succeeded:

• Build
• Check all files imported
• Lint style