fix tests

Author: kim-em

tests/lean/arrayGetU.lean

@@ -1,5 +1,5 @@
 def f (a : Array Nat) (i : Nat) (v : Nat) (h : i < a.size) : Array Nat :=
-  a.set ⟨i, h⟩ (a.get ⟨i, h⟩ + v)
+  a.set i (a.get ⟨i, h⟩ + v)
 
 set_option pp.proofs true
 

tests/lean/run/heapSort.lean

@@ -132,7 +132,7 @@ def insertExtractMax {lt} (self : BinaryHeap α lt) (x : α) : α × BinaryHeap
   | none => (x, self)
   | some m =>
     if lt x m then
-      let a := self.1.set ⟨0, size_pos_of_max e⟩ x
+      let a := self.1.set 0 x (size_pos_of_max e)
       (m, ⟨heapifyDown lt a ⟨0, by simp only [Array.size_set, a]; exact size_pos_of_max e⟩⟩)
     else (x, self)
 
@@ -141,16 +141,16 @@ def replaceMax {lt} (self : BinaryHeap α lt) (x : α) : Option α × BinaryHeap
   match e: self.max with
   | none => (none, ⟨self.1.push x⟩)
   | some m =>
-    let a := self.1.set ⟨0, size_pos_of_max e⟩ x
+    let a := self.1.set 0 x (size_pos_of_max e)
     (some m, ⟨heapifyDown lt a ⟨0, by simp only [Array.size_set, a]; exact size_pos_of_max e⟩⟩)
 
 /-- `O(log n)`. Replace the value at index `i` by `x`. Assumes that `x ≤ self.get i`. -/
 def decreaseKey {lt} (self : BinaryHeap α lt) (i : Fin self.size) (x : α) : BinaryHeap α lt where
-  arr := heapifyDown lt (self.1.set i x) ⟨i, by rw [self.1.size_set]; exact i.2⟩
+  arr := heapifyDown lt (self.1.set i x i.2) ⟨i, by rw [self.1.size_set]; exact i.2⟩
 
 /-- `O(log n)`. Replace the value at index `i` by `x`. Assumes that `self.get i ≤ x`. -/
 def increaseKey {lt} (self : BinaryHeap α lt) (i : Fin self.size) (x : α) : BinaryHeap α lt where
-  arr := heapifyUp lt (self.1.set i x) ⟨i, by rw [self.1.size_set]; exact i.2⟩
+  arr := heapifyUp lt (self.1.set i x i.2) ⟨i, by rw [self.1.size_set]; exact i.2⟩
 
 end BinaryHeap
 

tests/lean/run/inlineWithNestedRecIssue.lean

@@ -10,7 +10,7 @@ where
       if ptrEq a b then
         go (i+1) as
       else
-        go (i+1) (as.set ⟨i, h⟩ b)
+        go (i+1) (as.set i b)
     else
       return as
 

tests/lean/run/issue3204.lean

@@ -1,6 +1,6 @@
 def zero_out (arr : Array Nat) (i : Nat) : Array Nat :=
   if h : i < arr.size then
-    zero_out (arr.set ⟨i, h⟩ 0) (i + 1)
+    zero_out (arr.set i 0) (i + 1)
   else
     arr
 termination_by arr.size - i