From 81ae6a734bd3e36fa965a31c50c21d10eb31accf Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Thu, 13 Aug 2020 14:25:47 -0700
Subject: [PATCH] feat: mark `List.toArray` with `[matchPattern]`

---
 src/Init/Data/Array/Basic.lean | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

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