search

teorth / equational_theories

A project to map out the relations between different equational theories of Magmas.
https://teorth.github.io/equational_theories/
Apache License 2.0
212 stars 51 forks source link

DATA: Expand `Equations.lean` to contain the entire set of equations #37

Closed teorth closed 1 month ago

teorth commented 1 month ago

Of course, the equations that currently contain docstrings can keep those docstrings.

Hopefully there is a way to compile the resulting large file as an olean so that it does not slow down all subsequent lean verifications. See https://leanprover.zulipchat.com/#narrow/stream/458659-Equational/topic/Refactoring.20the.20Lean.20file.20structure for more discussion.

teorth commented 1 month ago

Completed in #48