Commit 2023-07-12 00:58 bb0602c3

View on Github →

feat: port Traversable deriving handlers (#5606)

Estimated changes

Modified Mathlib.lean

Modified Mathlib/Tactic.lean

Created Mathlib/Tactic/DeriveTraversable.lean

added def Mathlib.Deriving.Traversable.deriveFunctor

added def Mathlib.Deriving.Traversable.deriveLawfulFunctor

added def Mathlib.Deriving.Traversable.deriveLawfulTraversable

added def Mathlib.Deriving.Traversable.deriveTraversable

added def Mathlib.Deriving.Traversable.functorDeriveHandler

added def Mathlib.Deriving.Traversable.getAuxDefOfDeclName

added def Mathlib.Deriving.Traversable.getFVarIdsNotImplementationDetails

added def Mathlib.Deriving.Traversable.getFVarsNotImplementationDetails

added def Mathlib.Deriving.Traversable.higherOrderDeriveHandler

added def Mathlib.Deriving.Traversable.lawfulFunctorDeriveHandler

added def Mathlib.Deriving.Traversable.lawfulTraversableDeriveHandler

added def Mathlib.Deriving.Traversable.mapConstructor

added def Mathlib.Deriving.Traversable.mapField

added def Mathlib.Deriving.Traversable.mkCasesOnMatch

added def Mathlib.Deriving.Traversable.mkInstanceNameForTypeExpr

added def Mathlib.Deriving.Traversable.mkMap

added def Mathlib.Deriving.Traversable.mkOneInstance

added def Mathlib.Deriving.Traversable.mkTraverse

added def Mathlib.Deriving.Traversable.simpFunctorGoal

added def Mathlib.Deriving.Traversable.traversableDeriveHandler

added def Mathlib.Deriving.Traversable.traversableLawStarter

added def Mathlib.Deriving.Traversable.traverseConstructor

added def Mathlib.Deriving.Traversable.traverseField

Created test/Traversable.lean

added inductive Testing.Either

added structure Testing.MyStruct2

added structure Testing.MyStruct

added inductive Testing.MyTree

added inductive Testing.RecData

added def Testing.ex

added def Testing.x