Skip to content

feat: add well founded streams #1079

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom
Closed
wants to merge 2 commits into from
Closed

feat: add well founded streams #1079

wants to merge 2 commits into from

Conversation

fgdorais
Copy link
Collaborator

@fgdorais fgdorais commented Dec 25, 2024 •
edited
Loading

New attempt at well founded streams.

Note that the old Batteries.Data.Stream file was moved verbatim to Batteries.Data.Stream.Basic and now Batteries.Data.Stream is just an import file. These facts don't show well in the diff.

@github-actions github-actions bot added the awaiting-review This PR is ready for review; the author thinks it is ready to be merged. label Dec 25, 2024
@fgdorais fgdorais force-pushed the stream-wf branch 5 times, most recently from fb01ce0 to a08bbdb Compare December 25, 2024 22:01
leanprover-community-mathlib4-bot added a commit to leanprover-community/mathlib4 that referenced this pull request Dec 25, 2024
@leanprover-community-mathlib4-bot
Update Batteries branch for testing leanprover-community/batteries#1079
08e787a
leanprover-community-mathlib4-bot added a commit to leanprover-community/mathlib4 that referenced this pull request Dec 25, 2024
@leanprover-community-mathlib4-bot
Trigger CI for leanprover-community/batteries#1079
aa2377e
@leanprover-community-bot
Copy link
Collaborator

leanprover-community-bot commented Dec 25, 2024 •
edited
Loading

Mathlib CI status (docs):

@fgdorais
Copy link
Collaborator Author

@digama0 Your earlier attempt at well founded streams was too old to revive, so I started this new attempt from scratch. I surely missed some features from your PR #127 and I have diverged on some aspects. I would appreciate your review to make this attempt successful.

leanprover-community-mathlib4-bot added a commit to leanprover-community/mathlib4 that referenced this pull request Dec 25, 2024
@leanprover-community-mathlib4-bot
Trigger CI for leanprover-community/batteries#1079
716c0a2
@fgdorais fgdorais force-pushed the stream-wf branch 2 times, most recently from 07d50cd to a268e1c Compare December 25, 2024 23:39
leanprover-community-mathlib4-bot added a commit to leanprover-community/mathlib4 that referenced this pull request Dec 25, 2024
@leanprover-community-mathlib4-bot
Trigger CI for leanprover-community/batteries#1079
0274357
leanprover-community-mathlib4-bot added a commit to leanprover-community/mathlib4 that referenced this pull request Dec 26, 2024
@leanprover-community-mathlib4-bot
Trigger CI for leanprover-community/batteries#1079
a92672b
leanprover-community-mathlib4-bot added a commit to leanprover-community/mathlib4 that referenced this pull request Jan 5, 2025
@leanprover-community-mathlib4-bot
Trigger CI for leanprover-community/batteries#1079
046975b
@kim-em kim-em requested a review from digama0 January 30, 2025 01:38
@fgdorais fgdorais added awaiting-author Waiting for PR author to address issues and removed awaiting-review This PR is ready for review; the author thinks it is ready to be merged. labels Mar 9, 2025
@fgdorais
Copy link
Collaborator Author

Superseded by #1331

@fgdorais fgdorais closed this Jul 18, 2025
@github-actions github-actions bot removed the awaiting-author Waiting for PR author to address issues label Jul 18, 2025
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Reviewers

@digama0 digama0 Awaiting requested review from digama0

Assignees
No one assigned
Labels
builds-mathlib
Projects
None yet
Milestone
No milestone
Development

Successfully merging this pull request may close these issues.
2 participants
@fgdorais @leanprover-community-bot