A lean list of all equations?

Stream: Equational

[Amir Livne Bar-on]

Does it make sense to add a definition of "all laws"? This would help with statements such as "Eq2 implies ExN implies Eq1", and as an entry point for graph processing. Maybe as a map N -> EqN?

[Joachim Breitner]

I thought about this in the context of the “60%”. In the end I didn't need it – metacode can easily use Equation<n>, so the lean environment already is the map you are asking for. And non-meta code probably doesn't want to iterate over all equations anyways.

See for example the Facts G [1, 2] [4, 5] syntax proposed in https://github.com/teorth/equational_theories/pull/19, which expands the 1 here to Equation1.

I also don’t expect that the type checker will be particularly happy indexing into a long list, and you might run into slow proofs and deep recursion.

[Terence Tao]

There is a nascent plan equational#36 to create a class for magma expressions and equations, which would allow the ability to prove metatheorems about equations. I'm also beginning to collect these metatheorems in the blueprint.