Commit 2022-12-20 05:52 b9e19018

fix: Data.List.Defs (#1118) Fixes some problems surrounding Data.List.Defs that were affecting the ongoing port of Data.List.Basic.

• introduces takeI as a faithful port of take' and fixes the align
  • take' was previously erroneously aligned with takeD. takeD uses an explicitly-provided argument as a default whereas takeI usesInhabited's default.
• reverses the dependency Data.List.Chain → Data.List.Defs to Data.List.Defs → Data.List.Chain
  • This was causing a circular dependency for Data.List.Basic when it attempted to import Data.List.Defs.
  • We move chain_cons from Data.List.Chain into Data.List.Defs.
  • All of these changes are in keeping mathlib3's original structure.
  • We have to supplement Control.Traversable.Basic's imports, since it was previously relying on Data.Option.Defs via Data.List.Defs ← Data.List.Chain ← ... See this Zulip conversation for more context.