diff --git a/Batteries/Data/Array/Basic.lean b/Batteries/Data/Array/Basic.lean index 52e331bc7b..3f05693926 100644 --- 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 index 22f2874ed8..7f3e66e1a6 100644 --- 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