diff --git a/src/Init/Data/Array/Basic.lean b/src/Init/Data/Array/Basic.lean index 279c774391..af0a6fb236 100644 --- a/src/Init/Data/Array/Basic.lean +++ b/src/Init/Data/Array/Basic.lean @@ -717,7 +717,7 @@ export Array (mkArray) | [] => 0 | _::as => as.redLength + 1 -@[inline] def List.toArray {α : Type u} (as : List α) : Array α := +@[inline, matchPattern] def List.toArray {α : Type u} (as : List α) : Array α := as.toArrayAux (Array.mkEmpty as.redLength) namespace Array