Commit 2024-09-04 09:34 5bd8bde1

chore(ModelTheory/Order): Reorganization for future refactoring (#16338) Reorganizes the file ModelTheory/Order to allow for future refactoring, including making orderStructure no longer an instance. The new organization puts purely syntactical constructions first, and then separates out a separate section of results that use order instances to model-theoretic facts and data. This will make it easier to make orderStructure not a global instance, and introduce instances going the other direction, from model-theoretic instances to orders.