feat: add finite and well-founded streams by fgdorais · Pull Request #1331 · leanprover-community/batteries

fgdorais · 2025-07-18T11:07:04Z

Add classes for provably finite streams and connect streams with standard library iterators.

ghost · 2025-07-18T11:55:40Z

Mathlib CI status (docs):

✅ Mathlib branch batteries-pr-testing-1331 has successfully built against this PR. (2025-07-18 11:55:38) View Log

It appears that foldlM is not tail recursive.

kim-em · 2025-08-08T00:32:38Z

Could you explain how this relates to the core iterators? What is the use case that is not being filled by those?

fgdorais · 2025-09-02T04:23:49Z

Could you explain how this relates to the core iterators?

The connection with iterators was in a follow-up PR #1372. I've closed that one and merged with this one.

What is the use case that is not being filled by those?

The main purpose is to help people port their stream-based code to iterator-based code.

…t compatibility (#1601) Co-authored-by: Claude Opus 4.5 <noreply@anthropic.com>

Co-authored-by: Claude <noreply@anthropic.com>

Co-authored-by: Claude Opus 4.5 <noreply@anthropic.com>

Co-authored-by: mathlib4-bot <github-mathlib4-bot@leanprover.zulipchat.com> Co-authored-by: leanprover-community-mathlib4-bot <129911861+leanprover-community-mathlib4-bot@users.noreply.github.com> Co-authored-by: leanprover-community-mathlib4-bot <leanprover-community-mathlib4-bot@users.noreply.github.com> Co-authored-by: github-actions <github-actions@github.com> Co-authored-by: Kyle Miller <kmill31415@gmail.com> Co-authored-by: Johan Commelin <johan@commelin.net> Co-authored-by: Matthew Ballard <matt@mrb.email> Co-authored-by: Markus Himmel <markus@lean-fro.org> Co-authored-by: Mario Carneiro <di.gama@gmail.com> Co-authored-by: Sebastian Ullrich <sebasti@nullri.ch> Co-authored-by: Joachim Breitner <mail@joachim-breitner.de> Co-authored-by: Mac Malone <mac@lean-fro.org> Co-authored-by: Rob23oba <152706811+Rob23oba@users.noreply.github.com> Co-authored-by: Anne C.A. Baanen <vierkantor@vierkantor.com> Co-authored-by: Eric Wieser <wieser.eric@gmail.com> Co-authored-by: Paul Reichert <6992158+datokrat@users.noreply.github.com> Co-authored-by: Parth Shastri <31370288+cppio@users.noreply.github.com> Co-authored-by: Joseph Rotella <7482866+jrr6@users.noreply.github.com> Co-authored-by: François G. Dorais <fgdorais@gmail.com> Co-authored-by: Marc Huisinga <mhuisi@protonmail.com> Co-authored-by: Sebastian Graf <sgraf1337@gmail.com> Co-authored-by: Eric Wieser <efw@google.com> Co-authored-by: Claude Opus 4.5 <noreply@anthropic.com>

Co-authored-by: Claude Opus 4.5 <noreply@anthropic.com>

Co-authored-by: François G. Dorais <fgdorais@gmail.com>

…1648)

Co-authored-by: mathlib4-bot <github-mathlib4-bot@leanprover.zulipchat.com> Co-authored-by: leanprover-community-mathlib4-bot <129911861+leanprover-community-mathlib4-bot@users.noreply.github.com> Co-authored-by: leanprover-community-mathlib4-bot <leanprover-community-mathlib4-bot@users.noreply.github.com> Co-authored-by: Rob23oba <152706811+Rob23oba@users.noreply.github.com> Co-authored-by: Markus Himmel <markus@lean-fro.org> Co-authored-by: Johan Commelin <johan@commelin.net> Co-authored-by: Matthew Ballard <matt@mrb.email> Co-authored-by: Kyle Miller <kmill31415@gmail.com> Co-authored-by: Mario Carneiro <di.gama@gmail.com> Co-authored-by: Sebastian Ullrich <sebasti@nullri.ch> Co-authored-by: Joachim Breitner <mail@joachim-breitner.de> Co-authored-by: Mac Malone <mac@lean-fro.org> Co-authored-by: Anne C.A. Baanen <vierkantor@vierkantor.com> Co-authored-by: Paul Reichert <6992158+datokrat@users.noreply.github.com> Co-authored-by: Eric Wieser <wieser.eric@gmail.com> Co-authored-by: github-actions <github-actions@github.com> Co-authored-by: Parth Shastri <31370288+cppio@users.noreply.github.com> Co-authored-by: Joseph Rotella <7482866+jrr6@users.noreply.github.com> Co-authored-by: Sebastian Graf <sgraf1337@gmail.com> Co-authored-by: Marc Huisinga <mhuisi@protonmail.com> Co-authored-by: Eric Wieser <efw@google.com> Co-authored-by: François G. Dorais <fgdorais@gmail.com>

Co-authored-by: François G. Dorais <fgdorais@gmail.com>

…pairs. (#1507) Co-authored-by: François G. Dorais <fgdorais@gmail.com>

…t_failure (#1658)

This was missed in #1652, which migrated the other nightly-testing workflows from PAT to GitHub App. The test_mathlib workflow still referenced `secrets.MATHLIB4_BOT`, causing batteries-pr-testing branches to stop being created in mathlib4-nightly-testing. Co-Authored-By: Claude Opus 4.6 <noreply@anthropic.com>

This reverts commit 0cfcca7.

Co-authored-by: Claude Opus 4.6 <noreply@anthropic.com>

Co-authored-by: F. G. Dorais <fgdorais@gmail.com>

Co-authored-by: Claude Opus 4.5 <noreply@anthropic.com> Co-authored-by: François G. Dorais <fgdorais@gmail.com>

Co-authored-by: François G. Dorais <fgdorais@gmail.com>

Co-authored-by: Laurent Sartran <lsartran@google.com> Co-authored-by: F. G. Dorais <fgdorais@gmail.com>

Co-authored-by: François G. Dorais <fgdorais@gmail.com> Co-authored-by: Kim Morrison <477956+kim-em@users.noreply.github.com> Co-authored-by: Claude Opus 4.5 <noreply@anthropic.com> Co-authored-by: Gavin Zhao <gavinzhaojw@protonmail.com> Co-authored-by: Ruben Van de Velde <65514131+Ruben-VandeVelde@users.noreply.github.com> Co-authored-by: Eric Wieser <wieser.eric@gmail.com>

feat: add finite and well-founded streams

fe12c9a

github-actions bot added the awaiting-review This PR is ready for review; the author thinks it is ready to be merged. label Jul 18, 2025

fgdorais mentioned this pull request Jul 18, 2025

feat: add well founded streams #1079

Closed

ghost pushed a commit to leanprover-community/mathlib4-nightly-testing that referenced this pull request Jul 18, 2025

Update Batteries branch for testing leanprover-community/batteries#1331

32585f5

fgdorais requested a review from digama0 July 18, 2025 11:09

ghost added the builds-mathlib label Jul 18, 2025

fgdorais added 3 commits July 18, 2025 10:38

fix: shrink Stream.Finite namespace

3677c49

chore: add docs

b127466

feat: make foldl tail recursive

1ee871d

It appears that foldlM is not tail recursive.

fgdorais mentioned this pull request Jul 20, 2025

feat: add stream combinators #1334

Open

1 task

feat: add missing instances

84b75e1

fgdorais force-pushed the stream-finite branch from 5799b12 to 84b75e1 Compare July 26, 2025 18:46

fgdorais added 2 commits August 10, 2025 20:26

chore: merge main

309e479

feat: add StreamIterator type

2a1aba1

fgdorais mentioned this pull request Aug 11, 2025

feat: connect streams and iterators #1372

Closed

1 task

fgdorais added 4 commits August 15, 2025 08:13

feat: wellfounded streams to finite iterators

5051a12

feat: finite iterators to wellfounded streams

c15a3f5

chore: merge main

7392b76

chore: merge stream-iter

a325f01

fgdorais force-pushed the stream-finite branch from 7e1a97d to a325f01 Compare September 2, 2025 03:34

fgdorais added 2 commits October 4, 2025 19:47

docs: improve descriptions

6ee0114

chore: merge main

5461356

ghost added the merge-conflict This PR has merge conflicts with the `main` branch which must be resolved by the author. label Oct 21, 2025

fgdorais and others added 4 commits February 26, 2026 15:20

chore: forward port of lean4#10627 (#1433)

0435bd4

refactor: WF.recC: avoid reducing wfrec (#1449)

45e00d6

refactor: Fin.dfoldlM: avoid reducing wfrec (#1448)

0f8d6ef

refactor: Nat.sqrt: avoid reducing wfrec (#1447)

5c315e2

kim-em and others added 30 commits February 26, 2026 15:23

fix: encode spaces in library_note declaration names for export forma…

1d85704

…t compatibility (#1601) Co-authored-by: Claude Opus 4.5 <noreply@anthropic.com>

fix: Early runLinter exit with IO.Process.exit to avoid deadlock (#1621)

dae79f0

chore: clean up Batteries.Tactic.Lint (#1613)

fa90a1d

fix: code action for match (#1626)

6944a51

fix: address shellcheck warnings in create-adaptation-pr.sh (#1624)

2e11993

Co-authored-by: Claude <noreply@anthropic.com>

chore: bump toolchain to v4.27.0 (#1627)

8ee71a8

feat(Data/BitVec): add lemmas about pow on BitVec (#1608)

05ddcbf

fix: prevent duplicate Zulip posts in nightly failure workflow (#1630)

d5c4ff1

Co-authored-by: Claude Opus 4.5 <noreply@anthropic.com>

feat: add bool wf relation (#1639)

1b8accc

fix: look for last bot message when deduplicating Zulip posts (#1632)

6da11f3

Co-authored-by: Claude Opus 4.5 <noreply@anthropic.com>

feat: linter accepts multiple modules to lint (#1619)

0c81b72

Co-authored-by: François G. Dorais <fgdorais@gmail.com>

chore: restore AsciiCasing API (#1635)

f4ca22a

perf(Tactic/Alias): use MapDeclarationExtension (#1646)

e143cfa

chore: migrate merge-conflicts workflow to GitHub App (#1651)

1b0bf64

chore: migrate nightly-testing workflows to GitHub App (#1652)

727847f

fix: don't re-export everything every time in batteriesLinterExt (#…

9ef13b6

…1648)

feat: fix some issues with equals t => tac (#1291)

b485078

Co-authored-by: François G. Dorais <fgdorais@gmail.com>

feat: Add enumeration between list indicies and element-multiplicity …

81caea0

…pairs. (#1507) Co-authored-by: François G. Dorais <fgdorais@gmail.com>

chore(CI): regenerate app token before late checkout in nightly_detec…

62bae8b

…t_failure (#1658)

Revert "chore: migrate test_mathlib workflow to GitHub App"

c8d92a8

This reverts commit 0cfcca7.

chore: migrate test_mathlib workflow to GitHub App (#1666)

268820b

Co-authored-by: Claude Opus 4.6 <noreply@anthropic.com>

fix: IsChain style improvements and deprecation correction (#1663)

3aec2cc

Co-authored-by: F. G. Dorais <fgdorais@gmail.com>

feat: support simp?/simp_all?/dsimp? in squeeze_scope (#1604)

f2aaca1

Co-authored-by: Claude Opus 4.5 <noreply@anthropic.com> Co-authored-by: François G. Dorais <fgdorais@gmail.com>

chore: clean up implementation of batteriesLinterExt (#1661)

e87eb93

Co-authored-by: François G. Dorais <fgdorais@gmail.com>

fix: add missing initHeartbeats (#1037)

0d0e5d3

Co-authored-by: Laurent Sartran <lsartran@google.com> Co-authored-by: F. G. Dorais <fgdorais@gmail.com>

perf(NameMapAttribute): wrap in a Thunk (#1667)

ca26f68

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

feat: add finite and well-founded streams#1331

feat: add finite and well-founded streams#1331
fgdorais wants to merge 99 commits intomainfrom
stream-finite

fgdorais commented Jul 18, 2025 •

edited

Loading

Uh oh!

ghost commented Jul 18, 2025

Uh oh!

kim-em commented Aug 8, 2025

Uh oh!

fgdorais commented Sep 2, 2025

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

17 participants

Conversation

fgdorais commented Jul 18, 2025 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

ghost commented Jul 18, 2025

Uh oh!

kim-em commented Aug 8, 2025

Uh oh!

fgdorais commented Sep 2, 2025

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

17 participants

fgdorais commented Jul 18, 2025 •

edited

Loading