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

feat(library/init/data/array/basic): add Array.back

Browse source
This commit is contained in:
Leonardo de Moura 2019-04-10 08:56:42 -07:00
parent 1c73a4d089
commit 804ff74350
1 changed files with 3 additions and 0 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

3
library/init/data/array/basic.lean
View file

@ -77,6 +77,9 @@ a.index ⟨i.toNat, h⟩
def get [Inhabited α] (a : @& Array α) (i : @& Nat) : α :=
if h : i < a.size then a.index ⟨i, h⟩ else default α
def back [Inhabited α] (a : Array α) : α :=
a.get (a.size - 1)
def getOpt (a : Array α) (i : Nat) : Option α :=
if h : i < a.size then some (a.index ⟨i, h⟩) else none