Commit 2023-06-15 11:52 bb23b07e

View on Github →

feat: further functions on ListM (#3618)

Estimated changes

Modified Mathlib.lean

Modified Mathlib/Data/ListM/Basic.lean

added def ListM.fin

modified def ListM.fixl

added def ListM.ofArray

modified def ListM.range

Created Mathlib/Data/ListM/Split.lean

added def ListM.getUpToFirst

added def ListM.groupBy

added def ListM.splitAtBecomesTrue

added def ListM.splitWhile

Modified test/ListM.lean