Commit 2024-04-29 09:44 d64b17d9
View on Github →chore: split Algebra.Algebra.Basic (#12486)
Splits Algebra.Algebra.Defs
off Algebra.Algebra.Basic
. Most imports only need the Defs file, which has significantly smaller imports. The remaining Algebra.Algebra.Basic
is now a grab-bag of unrelated results, and should probably be split further or rehomed.
This is mostly motivated by the wasted effort during minimization upon encountering Algebra.Algebra.Basic.