[Merged by Bors] - chore: bump dependencies (upstream LazyList)#14778
[Merged by Bors] - chore: bump dependencies (upstream LazyList)#14778
Conversation
PR summary f6bd88e504
|
| File | Base Count | Head Count | Change |
|---|---|---|---|
| Mathlib.Data.LazyList.Basic | 354 | 356 | +2 (+0.56%) |
Import changes for all files
| Files | Import difference |
|---|---|
Mathlib.Data.LazyList.Basic |
2 |
Declarations diff
+ bind_singleton
+ get_mk
+ get_pure
- Mem
- Mem.decidable
- append_assoc
- append_bind
- append_nil
- attach
- bind
- decidableEq
- find
- forall_mem_cons
- init
- instance : Monad LazyList
- instance {α} : Membership α (LazyList α)
- instance {α} [Repr α] : Repr (LazyList α)
- interleave
- interleaveAll
- mem_cons
- mem_nil
- mfirst
- pmap
- reverse
- traverse
You can run this locally as follows
## summary with just the declaration names:
./scripts/declarations_diff.sh <optional_commit>
## more verbose report:
./scripts/declarations_diff.sh long <optional_commit>
Ruben-VandeVelde
left a comment
There was a problem hiding this comment.
maintainer merge
|
🚀 Pull request has been placed on the maintainer queue by Ruben-VandeVelde. |
| (bind_pure_comp := by | ||
| intro _ _ f xs | ||
| simp only [bind, Functor.map, pure, singleton] | ||
| induction xs using LazyList.traverse.induct (m := @Id) (f := f) with | ||
| | case1 => | ||
| simp only [Thunk.pure, LazyList.bind, LazyList.traverse, Id.pure_eq] | ||
| | case2 _ _ ih => | ||
| simp only [LazyList.bind, LazyList.traverse, Seq.seq, Id.map_eq, append, Thunk.pure] | ||
| rw [← ih] | ||
| simp [Thunk.pure, Thunk.get, append]) | ||
| (id_map := by | ||
| intro α xs | ||
| induction xs using LazyList.rec (motive_2 := fun xs => id <$> xs.get = xs) with | ||
| | nil => simp only [Functor.map, comp_id, LazyList.bind] | ||
| | cons h t _ => simp only [Functor.map, comp_id, bind_singleton] | ||
| | mk f _ => ext; simp_all) |
There was a problem hiding this comment.
Any particular reason you swapped the order of these?
There was a problem hiding this comment.
Matches the order of the arguments.
32073cd to
f6bd88e
Compare
|
bors d+ I edited the PR description to capture your zulip comment. |
|
✌️ semorrison can now approve this pull request. To approve and merge a pull request, simply reply with |
|
Oh, I see CI is done bors merge |
Also adjusts names arguments to `LawfulMonad.mk'` to match their actual order. For some reason the motive now has to be specified explicitly. I'm not really interested in understanding why, however, because this file, in Batteries and Mathlib is about to be deprecated on the grounds that LazyList is not currently being used, is not actually useful in practice without VM support (it was ported from Mathlib3, where it did have such support), and MLList supplies much of the functionality. Co-authored-by: Eric Wieser <wieser.eric@gmail.com>
|
Pull request successfully merged into master. Build succeeded: |
Also adjusts names arguments to
LawfulMonad.mk'to match their actual order.For some reason the motive now has to be specified explicitly.
I'm not really interested in understanding why, however, because this file, in Batteries and Mathlib is about to be deprecated on the grounds that LazyList is not currently being used, is not actually useful in practice without VM support (it was ported from Mathlib3, where it did have such support), and MLList supplies much of the functionality.