From f274aed7ae8d1addd3e70adaf3183ccc6e1ed43d Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Fran=C3=A7ois=20G=2E=20Dorais?= Date: Thu, 3 Oct 2024 05:14:29 -0400 Subject: [PATCH] fix: argument order and make abbrev (#975) --- Batteries/Data/Array/Basic.lean | 10 +++++----- 1 file changed, 5 insertions(+), 5 deletions(-) diff --git a/Batteries/Data/Array/Basic.lean b/Batteries/Data/Array/Basic.lean index ad6b8129e6..f25b5e091b 100644 --- a/Batteries/Data/Array/Basic.lean +++ b/Batteries/Data/Array/Basic.lean @@ -148,7 +148,7 @@ should prove the index bound. A proof by `get_elem_tactic` is provided as a default argument for `h`. This will perform the update destructively provided that `a` has a reference count of 1 when called. -/ -def setN (a : Array α) (i : Nat) (h : i < a.size := by get_elem_tactic) (x : α) : Array α := +abbrev setN (a : Array α) (i : Nat) (x : α) (h : i < a.size := by get_elem_tactic) : Array α := a.set ⟨i, h⟩ x /-- @@ -157,7 +157,7 @@ Uses `get_elem_tactic` to supply a proof that the indices are in range. `hi` and `hj` are both given a default argument `by get_elem_tactic`. This will perform the update destructively provided that `a` has a reference count of 1 when called. -/ -def swapN (a : Array α) (i j : Nat) +abbrev swapN (a : Array α) (i j : Nat) (hi : i < a.size := by get_elem_tactic) (hj : j < a.size := by get_elem_tactic) : Array α := Array.swap a ⟨i,hi⟩ ⟨j, hj⟩ @@ -166,8 +166,8 @@ def swapN (a : Array α) (i j : Nat) The old entry is returned alongwith the modified vector. Automatically generates proof of `i < a.size` with `get_elem_tactic` where feasible. -/ -def swapAtN (a : Array α) (i : Nat) (h : i < a.size := by get_elem_tactic) (x : α) : α × Array α := - swapAt a ⟨i,h⟩ x +abbrev swapAtN (a : Array α) (i : Nat) (x : α) (h : i < a.size := by get_elem_tactic) : + α × Array α := swapAt a ⟨i,h⟩ x /-- `eraseIdxN a i h` Removes the element at position `i` from a vector of length `n`. @@ -176,7 +176,7 @@ that the index is valid. This function takes worst case O(n) time because it has to backshift all elements at positions greater than i. -/ -def eraseIdxN (a : Array α) (i : Nat) (h : i < a.size := by get_elem_tactic) : Array α := +abbrev eraseIdxN (a : Array α) (i : Nat) (h : i < a.size := by get_elem_tactic) : Array α := a.feraseIdx ⟨i, h⟩ end Array