Commit 2023-06-21 05:19 98c34d9e

View on Github →

feat: port Control.Bitraversable.Instances (#5225)

Estimated changes

Modified Mathlib.lean

Modified Mathlib/Control/Bitraversable/Basic.lean

Created Mathlib/Control/Bitraversable/Instances.lean

added def Const.bitraverse

added def Prod.bitraverse

added def Sum.bitraverse

Modified Mathlib/Control/Bitraversable/Lemmas.lean