Array.get api change

leanprover · Nov 14, 2024 · 7644209 · 7644209
1 parent 676db5c
commit 7644209
Showing 1 changed file with 1 addition and 1 deletion.
diff --git a/src/Lean/Data/RArray.lean b/src/Lean/Data/RArray.lean
@@ -27,7 +27,7 @@ where
       .branch mid (go lb mid (by omega) (by omega)) (go mid ub (by omega) h2)
 
 def RArray.ofArray (xs : Array α) (h : 0 < xs.size) : RArray α :=
-  .ofFn (fun i => xs.get i) h
+  .ofFn (xs[·]) h
 
 /-- The correctness theorem for `ofFn` -/
 theorem RArray.get_ofFn {n : Nat} (f : Fin n → α) (h : 0 < n) (i : Fin n) :