Zulip Chat Archive

Stream: batteries

---

Topics:

• haskell typeclasses (7 messages, latest: Apr 02 2025 at 00:02)
• inherit_doc doesn't know about alias (6 messages, latest: Mar 27 2025 at 17:59)
• Unifying Batteries.HashMap and Std.HashMap. (173 messages, latest: Mar 27 2025 at 02:38)
• MonadSatisfying, SatisfiesM and monadic reasoning (1 message, latest: Feb 09 2025 at 09:19)
• #1104 feat: add LawfulBEq instance for Vector (1 message, latest: Feb 03 2025 at 13:23)
• proof_wanteds for monadic functions (5 messages, latest: Feb 01 2025 at 05:44)
• PR #1107 help needed with Satisfies (13 messages, latest: Jan 31 2025 at 20:50)
• Slices (3 messages, latest: Jan 21 2025 at 22:22)
• lean 6397 (6 messages, latest: Dec 18 2024 at 06:02)
• Generalize Fin.fold? (22 messages, latest: Dec 06 2024 at 23:13)
• Fin.Enum PR (44 messages, latest: Nov 25 2024 at 08:10)
• batteries PR adaptations (4 messages, latest: Nov 17 2024 at 06:20)
• MonadSatisfying class design (21 messages, latest: Nov 14 2024 at 20:58)
• UnionFind on nightly-testing (6 messages, latest: Nov 13 2024 at 07:37)
• #1034 feat: List.SatisfiesM_foldlM (4 messages, latest: Nov 13 2024 at 00:12)
• eraseDup keeps last, not first occurrence? (14 messages, latest: Nov 12 2024 at 06:48)
• Proofs involving Vector (30 messages, latest: Nov 01 2024 at 03:26)
• batteries#1020 adaptations (1 message, latest: Oct 31 2024 at 00:39)
• signature of modify functions (12 messages, latest: Oct 30 2024 at 18:24)
• Build fails (14 messages, latest: Oct 25 2024 at 14:12)
• List.modifyNth (4 messages, latest: Oct 23 2024 at 02:22)
• move Mathlib.Data.Prod.Basic to batteries (9 messages, latest: Oct 17 2024 at 01:40)
• Batteries releases and Batteries template for lake (21 messages, latest: Oct 15 2024 at 23:33)
• why do these cumbersome hypotheses keep showing up? (3 messages, latest: Oct 15 2024 at 17:36)
• ten unproved string theorems (76 messages, latest: Oct 15 2024 at 06:48)
• #lint panic (15 messages, latest: Oct 15 2024 at 00:51)
• do you think the following lemmas are useful? (3 messages, latest: Oct 14 2024 at 09:27)
• v4.13.0-rc1 (10 messages, latest: Oct 11 2024 at 10:05)
• lemma notation (25 messages, latest: Oct 08 2024 at 09:47)
• multiple goals (18 messages, latest: Oct 01 2024 at 00:58)
• Design of List.min? / Array.min? (14 messages, latest: Sep 29 2024 at 22:03)
• Upstreaming #help command? (14 messages, latest: Sep 29 2024 at 03:51)
• batteries#887 breaking Mathlib (75 messages, latest: Sep 28 2024 at 13:44)
• Large vector hangs (83 messages, latest: Sep 28 2024 at 03:54)
• Batteries and LEM (93 messages, latest: Sep 27 2024 at 12:08)
• Welcome New Batteries Maintainers! (4 messages, latest: Sep 25 2024 at 20:33)
• regular expression derivatives (20 messages, latest: Sep 25 2024 at 11:11)
• List.ofFn upstreaming? (14 messages, latest: Sep 25 2024 at 09:14)
• who will maintain batteries? (10 messages, latest: Sep 18 2024 at 02:29)
• Haskell Style Arrows (6 messages, latest: Aug 31 2024 at 10:55)
• Batteries#925 (9 messages, latest: Aug 18 2024 at 00:18)
• Gitpod prebuild (1 message, latest: Aug 17 2024 at 12:39)
• no more make (6 messages, latest: Aug 16 2024 at 07:19)
• Opening batteries fork in gitpod (117 messages, latest: Aug 15 2024 at 11:53)
• Heartbeat checks (2 messages, latest: Jul 22 2024 at 21:20)
• RFC: Arrays with fixed length (446 messages, latest: Jul 19 2024 at 21:37)
• Commit access to lean-pr-testing-branches (2 messages, latest: Jul 16 2024 at 14:40)
• tidying commit messages (19 messages, latest: Jul 09 2024 at 17:17)
• Upstreaming List.Sublist, Pairwise, and Nodup. (11 messages, latest: Jul 08 2024 at 11:45)
• String/Lemmas (24 messages, latest: Jun 30 2024 at 11:12)
• Requiring LawfulHashable for HashMap (5 messages, latest: Jun 27 2024 at 06:01)
• New problems with the simpNF linter (7 messages, latest: Jun 20 2024 at 06:32)
• Cleanup old issues? (2 messages, latest: Jun 17 2024 at 14:47)
• print discrimination tree keys (17 messages, latest: Jun 17 2024 at 14:00)
• Bump batteries to v4.9.0-rc2 (9 messages, latest: Jun 17 2024 at 13:33)
• PR backlog (213 messages, latest: Jun 11 2024 at 03:56)
• About the merge conflict bot (2 messages, latest: Jun 08 2024 at 10:54)
• depth first search (21 messages, latest: Jun 07 2024 at 14:32)
• Nat.lt_succ and Nat.lt_succ_iff coincide (13 messages, latest: Jun 07 2024 at 05:14)
• batteries#825 adaptations for nightly-2024-06-06 (3 messages, latest: Jun 06 2024 at 13:12)
• RFC: Object and ObjectArray types (32 messages, latest: May 30 2024 at 02:16)
• interval tree (18 messages, latest: May 29 2024 at 23:50)
• [Bad interaction of alias and deprecated (since := )](topic/Bad.20interaction.20of.20alias.20and.20deprecated.20(since.20.3A.3D.20).html) (6 messages, latest: May 25 2024 at 11:39)
• #eval evaluating type incorrect terms (11 messages, latest: May 24 2024 at 11:34)
• collection typeclasses (135 messages, latest: May 22 2024 at 17:11)
• unreachableTactic linter not suppressed by #guard_msgs (7 messages, latest: May 15 2024 at 00:53)
• Std -> Boost migration (162 messages, latest: May 14 2024 at 23:13)
• ✔ Top-level Batteries.lean (10 messages, latest: May 11 2024 at 03:21)
• batteries#784 (11 messages, latest: May 10 2024 at 06:10)
• lake test (5 messages, latest: May 09 2024 at 14:19)
• stream events (4 messages, latest: May 07 2024 at 08:16)
• Unused variable in Tactic/Where (2 messages, latest: May 06 2024 at 14:06)
• List.rotate vs List.rotateLeft (3 messages, latest: May 06 2024 at 11:50)
• v4.8.0-rc1 issue (29 messages, latest: May 05 2024 at 07:47)
• List.removeNth vs List.eraseIdx (8 messages, latest: May 04 2024 at 15:28)
• upstreaming of List/Array material (18 messages, latest: May 03 2024 at 04:01)
• datetime (15 messages, latest: May 02 2024 at 21:04)
• bump PR (8 messages, latest: May 01 2024 at 03:21)
• simp attributes in Std (32 messages, latest: Apr 30 2024 at 14:13)
• Union and SDiff instances for Std.RBSet (3 messages, latest: Apr 30 2024 at 06:51)
• assoclist model (15 messages, latest: Apr 23 2024 at 15:13)
• String.length_append (2 messages, latest: Apr 17 2024 at 14:31)
• #guard_msgs doesn't silence warnings (10 messages, latest: Apr 17 2024 at 03:31)
• List.get_zero (2 messages, latest: Apr 16 2024 at 04:19)
• upstream Std.Lean.Delaborator (7 messages, latest: Apr 15 2024 at 09:53)
• Movement from Std to Init (68 messages, latest: Apr 10 2024 at 04:17)
• RFC: List.take_drop and List.drop_take (45 messages, latest: Apr 03 2024 at 15:12)
• Sets (53 messages, latest: Apr 03 2024 at 00:41)
• Array.join vs Array.flatten (25 messages, latest: Mar 28 2024 at 11:44)
• naming inconsistencies (16 messages, latest: Mar 25 2024 at 02:21)
• findIdx? and indexOf? (12 messages, latest: Mar 17 2024 at 11:14)
• findIdx and indexOf (18 messages, latest: Mar 14 2024 at 03:52)
• v4.7.0-rc2 (4 messages, latest: Mar 12 2024 at 22:03)
• purpose of Array theorems (4 messages, latest: Mar 08 2024 at 20:28)
• nightly-testing-2024-02-20 (1 message, latest: Feb 20 2024 at 23:06)
• guard_msgs unsatisfiable (2 messages, latest: Feb 20 2024 at 10:10)
• Extensional equivalence for HashMap (13 messages, latest: Feb 16 2024 at 08:19)
• Using leaff to verify a refactor (18 messages, latest: Feb 15 2024 at 19:12)
• Remove ext attribute to Rat (11 messages, latest: Feb 09 2024 at 16:36)
• shake (3 messages, latest: Feb 07 2024 at 13:13)
• Insufficient number of targets (17 messages, latest: Feb 04 2024 at 21:20)
• omega did not find a contradiction (42 messages, latest: Feb 04 2024 at 02:53)
• Move #find command to Std? (96 messages, latest: Feb 01 2024 at 13:43)
• std4#571 (3 messages, latest: Feb 01 2024 at 10:16)
• Process for PRs depending on Lean PRs (17 messages, latest: Jan 28 2024 at 10:45)
• bot access (4 messages, latest: Jan 24 2024 at 11:42)
• eq_of_cmp_eq (12 messages, latest: Jan 19 2024 at 00:30)
• CI failure on main (9 messages, latest: Jan 18 2024 at 10:03)
• exfalso puzzle (11 messages, latest: Jan 18 2024 at 06:26)
• reorganization for omega (24 messages, latest: Jan 18 2024 at 03:26)
• scope of std (86 messages, latest: Jan 13 2024 at 01:56)
• ✔ List.ilast' (7 messages, latest: Jan 11 2024 at 19:59)
• simprocs (10 messages, latest: Jan 10 2024 at 21:59)
• show_term bug? (8 messages, latest: Jan 09 2024 at 02:54)
• obtain rfl not working when powers involved. (66 messages, latest: Jan 05 2024 at 14:29)
• Requirements for regex library (10 messages, latest: Jan 05 2024 at 11:48)
• permission to push to non-main branches (17 messages, latest: Jan 04 2024 at 05:44)
• ✔ permission to change labels (4 messages, latest: Jan 01 2024 at 20:02)
• v4.5.0-rc1 (2 messages, latest: Dec 21 2023 at 23:10)
• std4#470 (74 messages, latest: Dec 21 2023 at 11:41)
• lean-pr-testing-2964 conflicts with std4#466 (39 messages, latest: Dec 21 2023 at 11:29)
• std4#399 (9 messages, latest: Dec 21 2023 at 05:55)
• HashMap insert or modify (16 messages, latest: Dec 19 2023 at 02:23)
• Trythis code action title (7 messages, latest: Dec 16 2023 at 21:19)
• ✔ Can I change change at to change to ? (8 messages, latest: Dec 12 2023 at 07:16)
• Panics in Std.HashMap.find! (4 messages, latest: Dec 09 2023 at 08:06)
• Setting elements of arrays with GetElem (10 messages, latest: Dec 08 2023 at 21:37)
• Cacheless library search (1 message, latest: Dec 07 2023 at 03:17)
• Zero and One (8 messages, latest: Dec 02 2023 at 04:18)
• Mathlib bump for "Operations for bit representation of …" (40 messages, latest: Dec 01 2023 at 00:54)
• bump/v4.4.0 (25 messages, latest: Nov 30 2023 at 23:49)
• tail recursion (6 messages, latest: Nov 28 2023 at 03:34)
• Where to put lemmas (2 messages, latest: Nov 27 2023 at 18:38)
• ✔ Why is arithmetic in ℚ irreducible? (5 messages, latest: Nov 27 2023 at 11:44)
• no kernel reduction of HashMap.insert (20 messages, latest: Nov 25 2023 at 04:58)
• #354 (3 messages, latest: Nov 20 2023 at 08:47)
• register_label_attr and local attribute (2 messages, latest: Nov 19 2023 at 05:04)
• v4.3.0-rc2 (3 messages, latest: Nov 16 2023 at 11:21)
• linter.unusedVariables bug (2 messages, latest: Nov 14 2023 at 03:42)
• ✔ Exists.choose has the property (11 messages, latest: Nov 08 2023 at 21:48)
• NatCast (15 messages, latest: Nov 07 2023 at 17:40)
• CI (3 messages, latest: Nov 05 2023 at 04:59)
• upstreaming norm_cast (3 messages, latest: Nov 04 2023 at 17:54)
• v4.3.0-rc1 (2 messages, latest: Oct 31 2023 at 04:27)
• simp? suggestion includes comments (1 message, latest: Oct 26 2023 at 21:34)
• stable branch (11 messages, latest: Oct 25 2023 at 23:40)
• Changes to DiscrTree (10 messages, latest: Oct 23 2023 at 11:33)
• std4#215 Try these (8 messages, latest: Oct 23 2023 at 09:02)
• lake warnings about std (19 messages, latest: Oct 22 2023 at 21:46)
• Problem with repeat' (16 messages, latest: Oct 19 2023 at 08:14)
• Classical.not_forall (3 messages, latest: Oct 17 2023 at 09:29)
• oops (14 messages, latest: Oct 15 2023 at 11:42)
• eq_zero_of_add_eq_zero_right (6 messages, latest: Oct 09 2023 at 17:07)
• List.get?_eq_get and List.get!_eq_get (5 messages, latest: Sep 28 2023 at 20:07)
• Rename RBSet.map to RBSet.mapMonotonic? (3 messages, latest: Sep 26 2023 at 14:38)
• unused anonymous argument (10 messages, latest: Sep 19 2023 at 19:37)
• std4#160 case tactic, by type instead of by tag (14 messages, latest: Sep 13 2023 at 14:27)
• TryThis widget doesn't support multi-line suggestions (27 messages, latest: Sep 13 2023 at 00:57)
• Mathlib bump patches (92 messages, latest: Sep 06 2023 at 21:54)
• std doesn't work within mathlib any more (109 messages, latest: Sep 05 2023 at 18:24)
• std4#231, and code actions (10 messages, latest: Aug 26 2023 at 08:12)
• Triage role (16 messages, latest: Aug 25 2023 at 08:10)
• ToExpr derive handler (62 messages, latest: Aug 22 2023 at 02:12)
• try? from Mathlib.Control.Basic (9 messages, latest: Aug 21 2023 at 23:28)
• #6356 and docs#Nat.shiftLeft_eq (24 messages, latest: Aug 21 2023 at 21:49)
• compileTimeSearchPath% (3 messages, latest: Aug 20 2023 at 06:57)
• bump to nightly-2023-08-17 (1 message, latest: Aug 17 2023 at 09:45)
• How classical is std4? (56 messages, latest: Aug 16 2023 at 08:06)
• Equiv (63 messages, latest: Aug 14 2023 at 22:25)
• local instances in #lint (10 messages, latest: Aug 05 2023 at 10:40)
• New alias syntax (1 message, latest: Jul 31 2023 at 13:32)
• ✔ Failing code in test suite (6 messages, latest: Jul 29 2023 at 15:06)
• bump to nightly-2023-07-25 (8 messages, latest: Jul 28 2023 at 07:59)
• lint structure projections (86 messages, latest: Jul 26 2023 at 14:14)
• Cleanup Nat Lemmas (6 messages, latest: Jul 25 2023 at 10:04)
• Fin.succAbove (19 messages, latest: Jul 21 2023 at 01:11)
• bug in @\[ext\] with extends (6 messages, latest: Jul 19 2023 at 22:13)
• isn't "iff" obscure? (37 messages, latest: Jul 19 2023 at 21:40)
• Deque (8 messages, latest: Jul 17 2023 at 15:31)
• RFC: Positive integer type with views (9 messages, latest: Jul 17 2023 at 04:52)
• TacticCodeAction (13 messages, latest: Jul 12 2023 at 13:03)
• [Cmp typeclass refactor](topic/Cmp.20typeclass.20refactor.html) (20 messages, latest: Jul 10 2023 at 05:03)
• deprecated annotation (10 messages, latest: Jul 07 2023 at 18:09)
• Fin basics (206 messages, latest: Jul 07 2023 at 07:58)
• tailrec pmap (31 messages, latest: Jul 06 2023 at 05:20)
• Random calc ranges (11 messages, latest: Jul 05 2023 at 20:29)
• List.groupBy (35 messages, latest: Jul 03 2023 at 22:07)
• Unboxed Partial? (35 messages, latest: Jun 30 2023 at 07:30)
• prod_Nat.dvd_and_dvd_of_dvd_prod (3 messages, latest: Jun 29 2023 at 13:29)
• SAT core defs in Std? (31 messages, latest: Jun 29 2023 at 07:54)
• ✔ True = False be a goal (3 messages, latest: Jun 28 2023 at 13:13)
• proofs breaking in Std/Data/Array/Init/Lemmas.lean (2 messages, latest: Jun 28 2023 at 03:12)
• ListM (3 messages, latest: Jun 26 2023 at 06:01)
• LawfulBEq (1 message, latest: Jun 25 2023 at 17:36)
• Bug in extended binders? (9 messages, latest: Jun 25 2023 at 00:44)
• Bug with rcases combined with substitution (5 messages, latest: Jun 24 2023 at 00:46)
• https://github.com/leanprover/std4/pull/154 (8 messages, latest: Jun 19 2023 at 16:51)
• Bi-inhabited sort (1 message, latest: Jun 11 2023 at 06:21)
• Char.csize_pos and String.csize_pos are the same (13 messages, latest: May 29 2023 at 13:53)
• feat: move and add theorems on String std4#124 (17 messages, latest: May 11 2023 at 01:06)
• Porting just functionality (62 messages, latest: May 06 2023 at 15:58)
• repeat1' (4 messages, latest: Apr 17 2023 at 11:37)
• rcases? (4 messages, latest: Apr 09 2023 at 08:13)
• by_cases tags bug (4 messages, latest: Mar 31 2023 at 09:50)
• simp? bug (?) (16 messages, latest: Mar 30 2023 at 23:16)
• ✔ PR #98 (2 messages, latest: Mar 23 2023 at 11:29)
• Proving theorems about monads (32 messages, latest: Feb 28 2023 at 00:42)
• cache adoption by std4 (14 messages, latest: Feb 27 2023 at 01:01)
• nolinting generated decls (4 messages, latest: Feb 16 2023 at 18:11)
• low level UIntX and ByteArray stuff (4 messages, latest: Jan 27 2023 at 00:21)
• List.Perm in Std (19 messages, latest: Jan 26 2023 at 23:12)
• Std simp-nf decide props (9 messages, latest: Jan 22 2023 at 17:26)
• From/TryFrom as in Rust (15 messages, latest: Jan 20 2023 at 03:02)
• What lemmas do (not) belong to std? (5 messages, latest: Jan 18 2023 at 07:52)
• Stack & Queue (3 messages, latest: Jan 16 2023 at 12:37)
• Jannis' PRs (1 message, latest: Jan 09 2023 at 23:52)
• SetNotation naming conventions (2 messages, latest: Dec 31 2022 at 17:17)
• Nat.coprime (1 message, latest: Dec 22 2022 at 13:30)
• spurious unusedHavesSuffices linter error? (34 messages, latest: Dec 21 2022 at 10:54)
• just run one linter? (3 messages, latest: Dec 18 2022 at 20:49)
• requests for Rat (5 messages, latest: Dec 14 2022 at 12:25)
• local documentation? (40 messages, latest: Dec 02 2022 at 18:14)
• Pairing Heap (4 messages, latest: Dec 02 2022 at 05:27)
• online documentation? (5 messages, latest: Dec 02 2022 at 01:14)
• ext is weaker (8 messages, latest: Nov 24 2022 at 15:51)
• Move on_goal to std (1 message, latest: Nov 23 2022 at 12:04)
• bump to nightly-2022-11-17 (3 messages, latest: Nov 17 2022 at 11:41)
• New issues (1 message, latest: Nov 01 2022 at 23:58)
• [RFC] Renaming Std.Tactic (6 messages, latest: Oct 28 2022 at 11:23)
• Range folds (18 messages, latest: Oct 26 2022 at 22:10)
• documentation efforts (10 messages, latest: Oct 26 2022 at 07:22)
• Array lemmas (3 messages, latest: Oct 26 2022 at 03:12)
• ✔ functional streams from lean 3 (3 messages, latest: Oct 25 2022 at 14:25)
• About LawfulOrd (27 messages, latest: Oct 15 2022 at 07:58)
• RBSet functions (16 messages, latest: Oct 12 2022 at 13:27)
• ✔ BEq nonsense (25 messages, latest: Oct 11 2022 at 19:10)
• Build lists top-down (12 messages, latest: Oct 07 2022 at 02:34)
• operations on HashMap (7 messages, latest: Oct 06 2022 at 08:53)

---

Last updated: May 02 2025 at 03:31 UTC