From 8d2d43beb2aa9816d328f577fb3860dc90207916 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Sun, 7 Apr 2019 12:42:56 -0700
Subject: [PATCH] feat(library/init/data/array/basic): add shrink

---
 library/init/data/array/basic.lean | 6 ++++--
 1 file changed, 4 insertions(+), 2 deletions(-)

diff --git a/library/init/data/array/basic.lean b/library/init/data/array/basic.lean
index 9e6ec02b6b..ce2f7be32f 100644
--- a/library/init/data/array/basic.lean
+++ b/library/init/data/array/basic.lean
@@ -12,8 +12,6 @@ universes u v w
 The Compiler has special support for arrays.
 They are implemented using dynamic arrays: https://en.wikipedia.org/wiki/Dynamic_array
 -/
-
--- TODO(Leo): mark as opaque
 structure Array (α : Type u) :=
 (sz   : Nat)
 (data : Fin sz → α)
@@ -107,6 +105,10 @@ def pop (a : Array α) : Array α :=
 { sz   := Nat.pred a.sz,
   data := λ ⟨j, h⟩, a.index ⟨j, Nat.ltOfLtOfLe h (Nat.predLe _)⟩ }
 
+-- 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
+
 section
 variables {m : Type v → Type v} [Monad m]
 local attribute [instance] monadInhabited'