DeriveTraversable
📁 Source: Mathlib/Tactic/DeriveTraversable.lean
Statistics
Mathlib.Deriving.Traversable
Definitions
| Name | Category | Theorems |
|---|---|---|
deriveFunctor 📖 | CompOp | — |
deriveLawfulFunctor 📖 | CompOp | — |
deriveLawfulTraversable 📖 | CompOp | — |
deriveTraversable 📖 | CompOp | — |
functorDeriveHandler 📖 | CompOp | — |
getAuxDefOfDeclName 📖 | CompOp | — |
getFVarIdsNotImplementationDetails 📖 | CompOp | — |
getFVarsNotImplementationDetails 📖 | CompOp | — |
higherOrderDeriveHandler 📖 | CompOp | — |
lawfulFunctorDeriveHandler 📖 | CompOp | — |
lawfulTraversableDeriveHandler 📖 | CompOp | — |
mapConstructor 📖 | CompOp | — |
mapField 📖 | CompOp | — |
mkCasesOnMatch 📖 | CompOp | — |
mkInstanceNameForTypeExpr 📖 | CompOp | — |
mkMap 📖 | CompOp | — |
mkOneInstance 📖 | CompOp | — |
mkTraverse 📖 | CompOp | — |
nestedMap 📖 | CompOp | — |
nestedTraverse 📖 | CompOp | — |
simpFunctorGoal 📖 | CompOp | — |
traversableDeriveHandler 📖 | CompOp | — |
traversableLawStarter 📖 | CompOp | — |
traverseConstructor 📖 | CompOp | — |
traverseField 📖 | CompOp | — |
---