fix: use lambda

leanprover-community · Nov 25, 2024 · 6052abd · 6052abd
1 parent 8db191b
commit 6052abd
Show file tree

Hide file tree

Showing 2 changed files with 2 additions and 2 deletions.
diff --git a/Batteries/Data/Array/Basic.lean b/Batteries/Data/Array/Basic.lean
@@ -176,7 +176,7 @@ def eraseIdx! (a : Array α) (i : Nat) : Array α :=
     panic! s!"index {i} out of bounds"
 
 /-- `finRange n` is the array of all elements of `Fin n` in order. -/
-protected def finRange (n : Nat) : Array (Fin n) := ofFn id
+protected def finRange (n : Nat) : Array (Fin n) := ofFn fun i => i
 
 end Array
 

diff --git a/Batteries/Data/List/Basic.lean b/Batteries/Data/List/Basic.lean
@@ -1066,4 +1066,4 @@ where
   | b :: l, r => bif p b then reverseAux (a :: r) (b :: l) else loop l (b :: r)
 
 /-- `finRange n` lists all elements of `Fin n` in order -/
-def finRange (n : Nat) : List (Fin n) := ofFn id
+def finRange (n : Nat) : List (Fin n) := ofFn fun i => i