From acd482c5f252af13072f520bf31f6ef93aa6cf45 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Fri, 14 Jan 2022 19:47:42 -0800 Subject: [PATCH] feat: define `Array.modify` without using `Inhabited` --- src/Init/Data/Array/Basic.lean | 13 +++++++++++-- 1 file changed, 11 insertions(+), 2 deletions(-) diff --git a/src/Init/Data/Array/Basic.lean b/src/Init/Data/Array/Basic.lean index 187634cd87..483e0ca8c3 100644 --- a/src/Init/Data/Array/Basic.lean +++ b/src/Init/Data/Array/Basic.lean @@ -117,8 +117,17 @@ def modifyM [Monad m] [Inhabited α] (a : Array α) (i : Nat) (f : α → m α) pure a @[inline] -def modify [Inhabited α] (a : Array α) (i : Nat) (f : α → α) : Array α := - Id.run <| a.modifyM i f +unsafe def modifyUnsafe (a : Array α) (i : Nat) (f : α → α) : Array α := + if h : i < a.size then + let idx : Fin a.size := ⟨i, h⟩ + let v := a.get idx + let a' := a.set idx (unsafeCast ()) + a'.set (size_set a .. ▸ idx) (f v) + else + a + +@[implementedBy modifyUnsafe] +constant modify (a : Array α) (i : Nat) (f : α → α) : Array α @[inline] def modifyOp [Inhabited α] (self : Array α) (idx : Nat) (f : α → α) : Array α :=