max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

feat: define Array.modify without using Inhabited

Browse source
This commit is contained in:
Leonardo de Moura 2022-01-14 19:47:42 -08:00
parent 9c5668515c
commit acd482c5f2
1 changed files with 11 additions and 2 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

13
src/Init/Data/Array/Basic.lean
View file

@ -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 α :=