From d0ffecd4198ca9fd1815dd8e8910631be4852798 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Thu, 4 Feb 2021 20:39:28 -0800 Subject: [PATCH] chore: consistency Make sure `Array.all` and `Array.any` parameter order is similar to `List.all` and `List.any`. --- src/Init/Data/Array/Basic.lean | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/src/Init/Data/Array/Basic.lean b/src/Init/Data/Array/Basic.lean index 5c9897d541..6ee1012d1e 100644 --- a/src/Init/Data/Array/Basic.lean +++ b/src/Init/Data/Array/Basic.lean @@ -423,11 +423,11 @@ def getIdx? [BEq α] (a : Array α) (v : α) : Option Nat := a.findIdx? fun a => a == v @[inline] -def any (p : α → Bool) (as : Array α) (start := 0) (stop := as.size) : Bool := +def any (as : Array α) (p : α → Bool) (start := 0) (stop := as.size) : Bool := Id.run <| as.anyM p start stop @[inline] -def all (p : α → Bool) (as : Array α) (start := 0) (stop := as.size) : Bool := +def all (as : Array α) (p : α → Bool) (start := 0) (stop := as.size) : Bool := Id.run <| as.allM p start stop def contains [BEq α] (as : Array α) (a : α) : Bool :=