From 52b72c85bf99a31b4aa5444611e6bde62ffa8ba2 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Fri, 12 Apr 2019 09:03:20 -0700 Subject: [PATCH] fix(library/init/data/array/basic): typo --- library/init/data/array/basic.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/library/init/data/array/basic.lean b/library/init/data/array/basic.lean index 2f19f04650..4c369802e0 100644 --- a/library/init/data/array/basic.lean +++ b/library/init/data/array/basic.lean @@ -110,7 +110,7 @@ def pop (a : Array α) : Array α := -- TODO(Leo): justify termination using wf-rec partial def shrink : Array α → Nat → Array α -| a n := if a.size ≥ n then a else shrink a.pop n +| a n := if n ≥ a.size then a else shrink a.pop n section variables {m : Type v → Type v} [Monad m]