deriving `has_le`

Stream: general

[Sky Wilshaw]

Is there an attribute I can use to automatically derive has_le (or other related order typeclasses) on a structure or inductive?

[Kevin Buzzard]

You could try @[derive has_le], this definitely works for some data-carrying typeclasses like fintype but I'm not sure it would work for this, because how is Lean supposed to guess the definition you want?

[Sky Wilshaw]

Ah that makes sense, thanks. For context, I'm familiar with systems in other languages that just use lexicographic order in the fields of a structure.