Commit
This commit does not belong to any branch on this repository, and may belong to a fork outside of the repository.
…3197) `Array.set!` and `Array.swap!` are fairly similar operations, both modify an array, both take an index that it out of bounds. But they behave different; all of these return `true` ``` #eval #[1,2].set! 2 42 == #[1,2] -- with panic #reduce #[1,2].set! 2 42 == #[1,2] -- no panic #eval #[1,2].swap! 0 2 == #[1,2] -- with panic #reduce #[1,2].swap! 0 2 == default -- no panic ``` The implementations are ``` @[extern "lean_array_set"] def Array.set! (a : Array α) (i : @& Nat) (v : α) : Array α := Array.setD a i v ``` but ``` @[extern "lean_array_swap"] def swap! (a : Array α) (i j : @& Nat) : Array α := if h₁ : i < a.size then if h₂ : j < a.size then swap a ⟨i, h₁⟩ ⟨j, h₂⟩ else panic! "index out of bounds" else panic! "index out of bounds" ``` It seems to be more consistent to unify the behaviors, and define ``` @[extern "lean_array_swap"] def swap! (a : Array α) (i j : @& Nat) : Array α := if h₁ : i < a.size then if h₂ : j < a.size then swap a ⟨i, h₁⟩ ⟨j, h₂⟩ else a else a ``` Also adds docstrings. Fixes #3196
- Loading branch information