lean4-htt/src/Init/Data/List
Kim Morrison 1758b37a71
chore: List.filterMapM runs and returns left-to-right (#4820)
Closes #4676. Previously `List.filterMapM` was returning results
left-to-right, but evaluating right-to-left.
2024-07-24 09:00:10 +00:00
..
Attach.lean feat: upstream List.attach and Array.attach from Batteries (#4586) 2024-06-30 07:06:26 +00:00
Basic.lean feat: upstream more erase API (#4720) 2024-07-10 20:26:51 +00:00
BasicAux.lean chore: reorganisation of List API (#4469) 2024-06-17 04:21:53 +00:00
Control.lean chore: List.filterMapM runs and returns left-to-right (#4820) 2024-07-24 09:00:10 +00:00
Impl.lean feat: upstream more erase API (#4720) 2024-07-10 20:26:51 +00:00
Lemmas.lean fix: remove typeclass assumptions for Nodup.eraseP (#4790) 2024-07-21 07:51:42 +00:00
Notation.lean chore: reorganisation of List API (#4469) 2024-06-17 04:21:53 +00:00
TakeDrop.lean feat: lemmas for List.head and List.getLast (#4678) 2024-07-09 22:13:41 +00:00