Spelling of well-ordered type

Stream: mathlib4

[Sky Wilshaw]

What's the canonical spelling of a well-ordered type α? I can think of

1. αr : α → α → Prop with IsWellOrder α αr, but this doesn't come with decidable <
2. LinearOrder α and WellFoundedLT α, but then we don't get an IsWellOrder instance
   I think option 2 looks nicer, but I'm not aware if there's a mathlib convention.

[Yaël Dillies]

I doubt there is a convention indeed. But you can use [LinearOrder α] [IsWellOrder α (· < ·)].

[Yaël Dillies]

Probably we should have abbrev IsWellOrdered (α) [LT α] := IsWellOrder α (· < ·).

[Pedro Sánchez Terraf]

By the way (and out of curiosity, not an urgent business), are there "reflexive wellorders" in Mathlib?

[Sky Wilshaw]

I don't think there are, but you can achieve the effect with Preorder α and IsWellOrder α (· < ·).

[Yaël Dillies]

or {r : α → α → Prop} [IsRefl α r] [IsWellOrder α (fun a b, r a b ∧ ¬ r b a]

[Yaël Dillies]

Don't know exactly what kind of relations you care about, but I suspect everything can be smoothly done with what we already have.