Skip to content
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

feat: add well founded streams #1079

Open
wants to merge 1 commit into
base: main
Choose a base branch
from
Open

feat: add well founded streams #1079

wants to merge 1 commit into from
+423 −93

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
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Reviewers
No reviews
Assignees
No one assigned
Labels
awaiting-review This PR is ready for review; the author thinks it is ready to be merged. builds-mathlib
Projects
None yet
Milestone
No milestone
Development

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