batteries
batteries copied to clipboard
leanprover-community
feat: add well founded streams
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.
Mathlib CI status (docs):
- 🟡 Mathlib branch batteries-pr-testing-1079 build against this PR was cancelled. (2024-12-25 22:07:50) View Log
- ✅ Mathlib branch batteries-pr-testing-1079 has successfully built against this PR. (2024-12-25 22:48:32) View Log
- 🟡 Mathlib branch batteries-pr-testing-1079 build against this PR was cancelled. (2024-12-25 23:43:35) View Log
- ✅ Mathlib branch batteries-pr-testing-1079 has successfully built against this PR. (2024-12-26 00:26:07) View Log
- ✅ Mathlib branch batteries-pr-testing-1079 has successfully built against this PR. (2024-12-26 07:18:26) View Log
- 🟡 Mathlib branch batteries-pr-testing-1079 build against this PR was cancelled. (2025-01-05 09:22:20) View Log
@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.