feat: Array.swap takes Nat arguments, with tactic provided proofs

leanprover / lean4

Lean 4 programming language and theorem prover

https://lean-lang.org

Apache License 2.0

4.75k stars 427 forks source link

feat: Array.swap takes Nat arguments, with tactic provided proofs #6194

Closed kim-em closed 5 days ago

kim-em commented 5 days ago

This PR changes the signature of Array.swap, so it takes Nat arguments with tactic provided bounds checking. It also renames Array.swap! to Array.swapIfInBounds.

leanprover-community-bot commented 5 days ago

Mathlib CI status (docs):

💥 Mathlib branch lean-pr-testing-6194 build failed against this PR. (2024-11-24 06:39:58) View Log
🟡 Mathlib branch lean-pr-testing-6194 build against this PR was cancelled. (2024-11-24 07:37:40) View Log
✅ Mathlib branch lean-pr-testing-6194 has successfully built against this PR. (2024-11-24 08:14:19) View Log