Commit 2022-12-06 02:20 5bdee754

View on Github →

feat: port data.list.defs (#803) Port of data.list.defs, mostly consists of appropriate #aligns to map mathlib List functions to the appropriate definitions in Std4 Based on 1fc36cc9c8264e6e81253f88be7fb2cb6c92d76a

Estimated changes

Modified Mathlib.lean

Modified Mathlib/Control/Functor.lean

added def Functor.mapConstRev

Created Mathlib/Data/List/Defs.lean

added def List.All₂

added def List.alternatingProd

added def List.alternatingSum

added def List.andM

added def List.choose

added def List.chooseX

added def List.dedup

added def List.destutter'

added def List.destutter

added def List.erasep

added def List.extractp

added def List.findM

added def List.findM?'

added def List.foldlIdxM

added def List.foldrIdxM

added def List.getI

added def List.mapAsyncChunked

added def List.mapDiagM'

added def List.mapIdxM'

added def List.mapIdxMAux'

added def List.map₂Left'

added def List.map₂Left

added def List.map₂Right'

added def List.map₂Right

added def List.orM

added def List.permutations'

added def List.permutations'Aux

added def List.permutations

added def List.permutationsAux.rec

added def List.permutationsAux2

added def List.permutationsAux

added def List.prod

added def List.replaceIf

added def List.sublistsAux₁

added def List.sum

added def List.zipWith3

added def List.zipWith4

added def List.zipWith5