From 804ff743505620eff26969ce5f0caafc0da51981 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Wed, 10 Apr 2019 08:56:42 -0700 Subject: [PATCH] feat(library/init/data/array/basic): add `Array.back` --- library/init/data/array/basic.lean | 3 +++ 1 file changed, 3 insertions(+) diff --git a/library/init/data/array/basic.lean b/library/init/data/array/basic.lean index 78977a7d60..2f19f04650 100644 --- a/library/init/data/array/basic.lean +++ b/library/init/data/array/basic.lean @@ -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