Changing file structure

Stream: Equational

[Daniel Weber]

There are starting to be a lot of files in the top equational_theories, and I think it might make sense to split them to folder.
My suggestion:

• A Meta folder (or Tactic) for Lean metaprogramming: Closure, DecideBang, EquationalResult, EquationsCommand, FactsSyntax, MemoFinOp, ParseImplications, Superposition, Visualization.
• A Logic folder (or Meta) for logical results: Compactness, Completeness, Counting, FreeComm, FreeMagma, Homomorphisms, MagmaLaw, MagmaOp, OrderMetatheorem, Preorder
• I think the rest of the files could remain in the top level: AllEquations, Equations, Generated, InfModel, Magma, SmallMagmas, Subgraph, Z3Counterexamples

Does this look good?

[Shreyas Srinivas]

This is gigantic refactor

[Shreyas Srinivas]

A lot of PRs will break

[Andrés Goens]

is this just for aesthetics, or is there a technical benefit to the split?

[Terence Tao]

As a low-tech solution, I have made lists of human-generated Lean files in CONTRIBUTING.md, split somewhat arbitrarily into three categories vaguely resembling your proposal: "core files", which are used by other key components of the project; "technical files", which tend to revolve around tactics, parsing, and efficient data structures; and "contributed files", which are on various interesting magma topics but somewhat peripheral at present (though the duality files will likely get promoted to "core" at some point).

These lists are manually curated (mostly by myself), and so often lagging a few days the most recent codebase, but perhaps they are enough of a guide for now.