lean4 icon indicating copy to clipboard operation
lean4 copied to clipboard
verified publisher icon leanprover

refactor: move Std.Range to Std.Legacy.Range

Open datokrat opened this issue 1 month ago • 2 comments

This PR renames the namespace Std.Range to Std.Legacy.Range. Instead of using Std.Range and [a:b] notation, the new range type Std.Rco and its corresponding a...b notation should be used. There are also other ranges with open/closed/infinite boundary shapes in Std.Data.Range.Polymorphic and the new range notation also works for Int, Int8, UInt8, Fin etc.

datokrat avatar Dec 01 '25 10:12 datokrat

Mathlib CI status (docs):

  • ❗ Batteries CI can not be attempted yet, as the nightly-testing-2025-12-01 tag does not exist there yet. We will retry when you push more commits. If you rebase your branch onto nightly-with-mathlib, Batteries CI should run now. You can force Mathlib CI using the force-mathlib-ci label. (2025-12-01 12:02:03)
  • 💥 Mathlib branch lean-pr-testing-11438 build failed against this PR. (2025-12-04 18:21:29) View Log
  • ❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase 5339c47555cb65958259b1c4c4c687c3863a08be --onto 19e1fe55f33a8aadc4243da32828b70a4b4677cc. You can force Mathlib CI using the force-mathlib-ci label. (2025-12-13 00:18:06) Forcing Mathlib CI because the force-mathlib-ci label is present, despite problem: - ❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase 5339c47555cb65958259b1c4c4c687c3863a08be --onto 19e1fe55f33a8aadc4243da32828b70a4b4677cc. (2025-12-13 12:07:02)
  • 💥 Mathlib branch lean-pr-testing-11438 build failed against this PR. (2025-12-13 12:59:18) View Log
  • 🟡 Mathlib branch lean-pr-testing-11438 build this PR didn't complete normally. (2025-12-16 10:04:01) View Log

leanprover-community-bot avatar Dec 01 '25 12:12 leanprover-community-bot

Reference manual CI status:

  • ❗ Reference manual CI can not be attempted yet, as the nightly-testing-2025-12-01 tag does not exist there yet. We will retry when you push more commits. If you rebase your branch onto nightly-with-manual, reference manual CI should run now. You can force reference manual CI using the force-manual-ci label. (2025-12-01 12:02:05)
  • 💥 Reference manual branch lean-pr-testing-11438 build failed against this PR. (2025-12-04 17:36:38) View Log
  • 🟡 Reference manual branch lean-pr-testing-11438 build against this PR didn't complete normally. (2025-12-04 17:37:23) View Log
  • ✅ Reference manual branch lean-pr-testing-11438 has successfully built against this PR. (2025-12-12 23:14:14) View Log
  • 🟡 Reference manual branch lean-pr-testing-11438 build against this PR didn't complete normally. (2025-12-12 23:15:45) View Log
  • ❗ Reference manual CI will not be attempted unless your PR branches off the nightly-with-manual branch. Try git rebase 5339c47555cb65958259b1c4c4c687c3863a08be --onto 646df6ba16b3f68de539a085456c323e160e206d. You can force reference manual CI using the force-manual-ci label. (2025-12-13 00:18:07)
  • ❗ Reference manual CI can not be attempted yet, as the nightly-testing-2025-12-15 tag does not exist there yet. We will retry when you push more commits. If you rebase your branch onto nightly-with-manual, reference manual CI should run now. You can force reference manual CI using the force-manual-ci label. (2025-12-16 10:01:46)

leanprover-bot avatar Dec 01 '25 12:12 leanprover-bot