Refactoring Orders in Model Theory

Stream: mathlib4

[Aaron Anderson]

I'm trying to prove that countable dense linear orders are Fraïssé limits. I've got the first part of it, showing that the age of such a structure is the set of finite linear orders, at branch#dlo_age
In order to do this, I've had to refactor a whole bunch of the file on orders in model theory, and in particular there are a lot of weird instances and local instances. I'll hopefully isolate a PRs about just the refactor soon, but before I get there, I figured I'd share the project as it is, to see if anyone has any comments.

[Aaron Anderson]

@Yaël Dillies @Floris van Doorn @Johan Commelin @Chris Hughes @Eric Wieser might be interested.

[Aaron Anderson]

I hope that we can learn some lessons about this API and move closer to a design that would also generalize well to algebraic structures and graphs.

[Yaël Dillies]

Yes, I am interested to see the PRs