Commit 2023-08-09 01:11 aa94d2e4

View on Github →

chore: bump Std (adapt to migration of ListM) (#6413) ListM has been moved to Std and renamed as MLList. There are some slight API functions, that ensure operations are lazy, requiring the addition of some fun _ => here in Mathlib.

Estimated changes

deleted def ListM.asArray
deleted def ListM.cases'
deleted def ListM.concat
deleted def ListM.cons'
deleted def ListM.cons
deleted def ListM.drop
deleted def ListM.enum
deleted def ListM.filter
deleted def ListM.filterMap
deleted def ListM.fin
deleted def ListM.first
deleted def ListM.firstM
deleted def ListM.fixl
deleted def ListM.folds
deleted def ListM.head
deleted def ListM.head?
deleted def ListM.isEmpty
deleted def ListM.map
deleted def ListM.monadLift
deleted def ListM.nil
deleted def ListM.ofArray
deleted def ListM.ofList
deleted def ListM.ofListM
deleted def ListM.range
deleted def ListM.runState'
deleted def ListM.squash
deleted def ListM.takeUpToFirst
deleted def ListM.takeWhile
deleted def ListM.uncons
deleted def ListM
modified def bestFirstSearch
deleted def ListM.lines
deleted def ListM.runCmd
added def MLList.lines
added def MLList.runCmd
deleted def ListM.getUpToFirst
deleted def ListM.groupBy
deleted def ListM.splitWhile
added def MLList.groupBy
modified def l1
modified def l2
modified def ll
modified def nbhd