chore: rename Array.back to back!

src/Init/Data/Array/Basic.lean

@@ -235,9 +235,11 @@ def range (n : Nat) : Array Nat :=
 def singleton (v : α) : Array α :=
   mkArray 1 v
 
-def back [Inhabited α] (a : Array α) : α :=
+def back! [Inhabited α] (a : Array α) : α :=
   a.get! (a.size - 1)
 
+@[deprecated back! (since := "2024-10-31")] abbrev back := @back!
+
 def get? (a : Array α) (i : Nat) : Option α :=
   if h : i < a.size then some a[i] else none
 

src/Init/Data/Array/BinSearch.lean

@@ -69,8 +69,8 @@ namespace Array
   if as.isEmpty then do let v ← add (); pure <| as.push v
   else if lt k (as.get! 0) then do let v ← add (); pure <| as.insertAt! 0 v
   else if !lt (as.get! 0) k then as.modifyM 0 <| merge
-  else if lt as.back k then do let v ← add (); pure <| as.push v
-  else if !lt k as.back then as.modifyM (as.size - 1) <| merge
+  else if lt as.back! k then do let v ← add (); pure <| as.push v
+  else if !lt k as.back! then as.modifyM (as.size - 1) <| merge
   else binInsertAux lt merge add as k 0 (as.size - 1)
 
 @[inline] def binInsert {α : Type u} (lt : α → α → Bool) (as : Array α) (k : α) : Array α :=

src/Init/Data/Array/Lemmas.lean

@@ -105,8 +105,8 @@ We prefer to pull `List.toArray` outwards.
 
 @[simp] theorem toArray_singleton (a : α) : (List.singleton a).toArray = singleton a := rfl
 
-@[simp] theorem back_toArray [Inhabited α] (l : List α) : l.toArray.back = l.getLast! := by
-  simp only [back, size_toArray, Array.get!_eq_getElem!, getElem!_toArray, getLast!_eq_getElem!]
+@[simp] theorem back!_toArray [Inhabited α] (l : List α) : l.toArray.back! = l.getLast! := by
+  simp only [back!, size_toArray, Array.get!_eq_getElem!, getElem!_toArray, getLast!_eq_getElem!]
 
 @[simp] theorem forIn'_loop_toArray [Monad m] (l : List α) (f : (a : α) → a ∈ l.toArray → β → m (ForInStep β)) (i : Nat)
     (h : i ≤ l.length) (b : β) :
@@ -495,14 +495,14 @@ theorem getElem?_eq_some_iff {as : Array α} : as[n]? = some a ↔ ∃ h : n < a
   cases as
   simp [List.getElem?_eq_some_iff]
 
-theorem back_eq_back? [Inhabited α] (a : Array α) : a.back = a.back?.getD default := by
-  simp only [back, get!_eq_getElem?, get?_eq_getElem?, back?]
+theorem back!_eq_back? [Inhabited α] (a : Array α) : a.back! = a.back?.getD default := by
+  simp only [back!, get!_eq_getElem?, get?_eq_getElem?, back?]
 
 @[simp] theorem back?_push (a : Array α) : (a.push x).back? = some x := by
   simp [back?, getElem?_eq_getElem?_toList]
 
-@[simp] theorem back_push [Inhabited α] (a : Array α) : (a.push x).back = x := by
-  simp [back_eq_back?]
+@[simp] theorem back!_push [Inhabited α] (a : Array α) : (a.push x).back! = x := by
+  simp [back!_eq_back?]
 
 theorem getElem?_push_lt (a : Array α) (x : α) (i : Nat) (h : i < a.size) :
     (a.push x)[i]? = some a[i] := by
@@ -615,8 +615,8 @@ theorem eq_empty_of_size_eq_zero {as : Array α} (h : as.size = 0) : as = #[] :=
   · simp [h]
   · intros; contradiction
 
-theorem eq_push_pop_back_of_size_ne_zero [Inhabited α] {as : Array α} (h : as.size ≠ 0) :
-    as = as.pop.push as.back := by
+theorem eq_push_pop_back!_of_size_ne_zero [Inhabited α] {as : Array α} (h : as.size ≠ 0) :
+    as = as.pop.push as.back! := by
   apply ext
   · simp [Nat.sub_add_cancel (Nat.zero_lt_of_ne_zero h)]
   · intros i h h'
@@ -625,12 +625,12 @@ theorem eq_push_pop_back_of_size_ne_zero [Inhabited α] {as : Array α} (h : as.
     else
       have heq : i = as.pop.size :=
         Nat.le_antisymm (size_pop .. ▸ Nat.le_pred_of_lt h) (Nat.le_of_not_gt hlt)
-      cases heq; rw [getElem_push_eq, back, ←size_pop, get!_eq_getD, getD, dif_pos h]; rfl
+      cases heq; rw [getElem_push_eq, back!, ←size_pop, get!_eq_getD, getD, dif_pos h]; rfl
 
 theorem eq_push_of_size_ne_zero {as : Array α} (h : as.size ≠ 0) :
     ∃ (bs : Array α) (c : α), as = bs.push c :=
   let _ : Inhabited α := ⟨as[0]⟩
-  ⟨as.pop, as.back, eq_push_pop_back_of_size_ne_zero h⟩
+  ⟨as.pop, as.back!, eq_push_pop_back!_of_size_ne_zero h⟩
 
 theorem size_eq_length_toList (as : Array α) : as.size = as.toList.length := rfl
 
@@ -1621,6 +1621,8 @@ theorem toArray_concat {as : List α} {x : α} :
   apply ext'
   simp
 
+@[deprecated back!_toArray (since := "2024-10-31")] abbrev back_toArray := @back!_toArray
+
 end List
 
 namespace Array
@@ -1761,4 +1763,9 @@ abbrev get_swap := @getElem_swap
 @[deprecated getElem_swap' (since := "2024-09-30")]
 abbrev get_swap' := @getElem_swap'
 
+@[deprecated back!_eq_back? (since := "2024-10-31")] abbrev back_eq_back? := @back!_eq_back?
+@[deprecated back!_push (since := "2024-10-31")] abbrev back_push := @back!_push
+@[deprecated eq_push_pop_back!_of_size_ne_zero (since := "2024-10-31")]
+abbrev eq_push_pop_back_of_size_ne_zero := @eq_push_pop_back!_of_size_ne_zero
+
 end Array

src/Lean/Compiler/IR/ElimDeadVars.lean

@@ -13,7 +13,7 @@ partial def reshapeWithoutDead (bs : Array FnBody) (term : FnBody) : FnBody :=
   let rec reshape (bs : Array FnBody) (b : FnBody) (used : IndexSet) :=
     if bs.isEmpty then b
     else
-      let curr := bs.back
+      let curr := bs.back!
       let bs   := bs.pop
       let keep (_ : Unit) :=
         let used := curr.collectFreeIndices used

src/Lean/Compiler/IR/EmitLLVM.lean

@@ -1075,7 +1075,7 @@ def emitSetTag (builder : LLVM.Builder llvmctx) (x : VarId) (i : Nat) : M llvmct
 def ensureHasDefault' (alts : Array Alt) : Array Alt :=
   if alts.any Alt.isDefault then alts
   else
-    let last := alts.back
+    let last := alts.back!
     let alts := alts.pop
     alts.push (Alt.default last.body)
 

src/Lean/Compiler/IR/ExpandResetReuse.lean

@@ -56,7 +56,7 @@ partial def eraseProjIncForAux (y : VarId) (bs : Array FnBody) (mask : Mask) (ke
   let keepInstr (b : FnBody) := eraseProjIncForAux y bs.pop mask (keep.push b)
   if bs.size < 2 then done ()
   else
-    let b := bs.back
+    let b := bs.back!
     match b with
     | .vdecl _ _ (.sproj _ _ _) _ => keepInstr b
     | .vdecl _ _ (.uproj _ _) _   => keepInstr b

src/Lean/Compiler/IR/PushProj.lean

@@ -13,7 +13,7 @@ namespace Lean.IR
 partial def pushProjs (bs : Array FnBody) (alts : Array Alt) (altsF : Array IndexSet) (ctx : Array FnBody) (ctxF : IndexSet) : Array FnBody × Array Alt :=
   if bs.isEmpty then (ctx.reverse, alts)
   else
-    let b    := bs.back
+    let b    := bs.back!
     let bs   := bs.pop
     let done (_ : Unit) := (bs.push b ++ ctx.reverse, alts)
     let skip (_ : Unit) := pushProjs bs alts altsF (ctx.push b) (b.collectFreeIndices ctxF)

src/Lean/Compiler/IR/SimpCase.lean

@@ -13,8 +13,8 @@ def ensureHasDefault (alts : Array Alt) : Array Alt :=
   if alts.any Alt.isDefault then alts
   else if alts.size < 2 then alts
   else
-    let last := alts.back;
-    let alts := alts.pop;
+    let last := alts.back!
+    let alts := alts.pop
     alts.push (Alt.default last.body)
 
 private def getOccsOf (alts : Array Alt) (i : Nat) : Nat := Id.run do

src/Lean/Data/Lsp/Utf16.lean

@@ -70,7 +70,7 @@ private def lineStartPos (text : FileMap) (line : Nat) : String.Pos :=
   else if text.positions.isEmpty then
     0
   else
-    text.positions.back
+    text.positions.back!
 
 /-- Computes an UTF-8 offset into `text.source`
 from an LSP-style 0-indexed (ln, col) position. -/

src/Lean/Data/Position.lean

@@ -66,12 +66,12 @@ partial def ofString (s : String) : FileMap :=
       let i := s.next i
       if c == '\n' then loop i (line+1) (ps.push i)
       else loop i line ps
-  loop 0 1 (#[0])
+  loop 0 1 #[0]
 
 partial def toPosition (fmap : FileMap) (pos : String.Pos) : Position :=
   match fmap with
   | { source := str, positions := ps } =>
-    if ps.size >= 2 && pos <= ps.back then
+    if ps.size >= 2 && pos <= ps.back! then
       let rec toColumn (i : String.Pos) (c : Nat) : Nat :=
         if i == pos || str.atEnd i then c
         else toColumn (str.next i) (c+1)
@@ -84,14 +84,14 @@ partial def toPosition (fmap : FileMap) (pos : String.Pos) : Position :=
           if pos == posM then { line := fmap.getLine m, column := 0 }
           else if pos > posM then loop m e
           else loop b m
-      loop 0 (ps.size -1)
+      loop 0 (ps.size - 1)
     else if ps.isEmpty then
       ⟨0, 0⟩
     else
       -- Some systems like the delaborator use synthetic positions without an input file,
       -- which would violate `toPositionAux`'s invariant.
       -- Can also happen with EOF errors, which are not strictly inside the file.
-      ⟨fmap.getLastLine, (pos - ps.back).byteIdx⟩
+      ⟨fmap.getLastLine, (pos - ps.back!).byteIdx⟩
 
 /-- Convert a `Lean.Position` to a `String.Pos`. -/
 def ofPosition (text : FileMap) (pos : Position) : String.Pos :=
@@ -101,7 +101,7 @@ def ofPosition (text : FileMap) (pos : Position) : String.Pos :=
     else if text.positions.isEmpty then
       0
     else
-      text.positions.back
+      text.positions.back!
   String.Iterator.nextn ⟨text.source, colPos⟩ pos.column |>.pos
 
 /--

src/Lean/Data/Xml/Parser.lean

@@ -463,7 +463,7 @@ mutual
     let mut res := #[]
     for x in xs do
       if res.size > 0 then
-        match res.back, x with
+        match res.back!, x with
         | Content.Character x, Content.Character y => res := res.set! (res.size - 1) (Content.Character $ x ++ y)
         | _, x => res := res.push x
       else res := res.push x

src/Lean/Elab/Arg.lean

@@ -39,7 +39,7 @@ partial def expandArgs (args : Array Syntax) : MetaM (Array NamedArg × Array Ar
   let (args, ellipsis) :=
     if args.isEmpty then
       (args, false)
-    else if args.back.isOfKind ``Lean.Parser.Term.ellipsis then
+    else if args.back!.isOfKind ``Lean.Parser.Term.ellipsis then
       (args.pop, true)
     else
       (args, false)

src/Lean/Elab/BuiltinNotation.lean

@@ -226,7 +226,7 @@ partial def mkPairs (elems : Array Term) : MacroM Term :=
       loop i acc
     else
       pure acc
-  loop (elems.size - 1) elems.back
+  loop (elems.size - 1) elems.back!
 
 /-- Return syntax `PProd.mk elems[0] (PProd.mk elems[1] ... (PProd.mk elems[elems.size - 2] elems[elems.size - 1])))` -/
 partial def mkPPairs (elems : Array Term) : MacroM Term :=
@@ -238,7 +238,7 @@ partial def mkPPairs (elems : Array Term) : MacroM Term :=
       loop i acc
     else
       pure acc
-  loop (elems.size - 1) elems.back
+  loop (elems.size - 1) elems.back!
 
 /-- Return syntax `MProd.mk elems[0] (MProd.mk elems[1] ... (MProd.mk elems[elems.size - 2] elems[elems.size - 1])))` -/
 partial def mkMPairs (elems : Array Term) : MacroM Term :=
@@ -250,7 +250,7 @@ partial def mkMPairs (elems : Array Term) : MacroM Term :=
       loop i acc
     else
       pure acc
-  loop (elems.size - 1) elems.back
+  loop (elems.size - 1) elems.back!
 
 
 open Parser in

src/Lean/Elab/Calc.lean

@@ -136,7 +136,7 @@ def throwCalcFailure (steps : Array CalcStepView) (expectedType result : Expr) :
           but is expected to be{indentD m!"{elhs} : {← inferType elhs}"}"
         failed := true
       unless ← isDefEqGuarded rhs erhs do
-        logErrorAt steps.back.term m!"\
+        logErrorAt steps.back!.term m!"\
           invalid 'calc' step, right-hand side is{indentD m!"{rhs} : {← inferType rhs}"}\n\
           but is expected to be{indentD m!"{erhs} : {← inferType erhs}"}"
         failed := true

src/Lean/Elab/Do.lean

@@ -801,7 +801,7 @@ private def mkTuple (elems : Array Syntax) : MacroM Syntax := do
   else if elems.size == 1 then
     return elems[0]!
   else
-    elems.extract 0 (elems.size - 1) |>.foldrM (init := elems.back) fun elem tuple =>
+    elems.extract 0 (elems.size - 1) |>.foldrM (init := elems.back!) fun elem tuple =>
       ``(MProd.mk $elem $tuple)
 
 /-- Return `some action` if `doElem` is a `doExpr <action>`-/

src/Lean/Elab/Level.lean

@@ -60,11 +60,11 @@ partial def elabLevel (stx : Syntax) : LevelElabM Level := withRef stx do
     elabLevel (stx.getArg 1)
   else if kind == ``Lean.Parser.Level.max then
     let args := stx.getArg 1 |>.getArgs
-    args[:args.size - 1].foldrM (init := ← elabLevel args.back) fun stx lvl =>
+    args[:args.size - 1].foldrM (init := ← elabLevel args.back!) fun stx lvl =>
       return mkLevelMax' (← elabLevel stx) lvl
   else if kind == ``Lean.Parser.Level.imax then
     let args := stx.getArg 1 |>.getArgs
-    args[:args.size - 1].foldrM (init := ← elabLevel args.back) fun stx lvl =>
+    args[:args.size - 1].foldrM (init := ← elabLevel args.back!) fun stx lvl =>
       return mkLevelIMax' (← elabLevel stx) lvl
   else if kind == ``Lean.Parser.Level.hole then
     mkFreshLevelMVar

src/Lean/Elab/PreDefinition/Structural/IndGroupInfo.lean

@@ -105,6 +105,6 @@ def IndGroupInst.nestedTypeFormers (igi : IndGroupInst) : MetaM (Array Expr) :=
   auxMotives.mapM fun motive =>
     forallTelescopeReducing motive fun xs _ => do
       assert! xs.size > 0
-      mkForallFVars xs.pop (← inferType xs.back)
+      mkForallFVars xs.pop (← inferType xs.back!)
 
 end Lean.Elab.Structural

src/Lean/Elab/PreDefinition/TerminationArgument.lean

@@ -118,7 +118,7 @@ def TerminationArgument.delab (arity : Nat) (extraParams : Nat) (termArg : Termi
         Array.map (fun (i : Ident) => if stxBody.raw.hasIdent i.getId then i else hole) vars
       -- drop trailing underscores
       let mut vars := vars
-      while ! vars.isEmpty && vars.back.raw.isOfKind ``hole do vars := vars.pop
+      while ! vars.isEmpty && vars.back!.raw.isOfKind ``hole do vars := vars.pop
       if termArg.structural then
         if vars.isEmpty then
           `(terminationBy|termination_by structural $stxBody)

src/Lean/Elab/Quotation.lean

@@ -190,7 +190,7 @@ private partial def quoteSyntax : Syntax → TermElabM Term
                 | $[some $ids:ident],* => $(quote inner)
                 | $[_%$ids],*          => Array.empty)
             | _ =>
-              let arr ← ids[:ids.size-1].foldrM (fun id arr => `(Array.zip $id:ident $arr)) ids.back
+              let arr ← ids[:ids.size-1].foldrM (fun id arr => `(Array.zip $id:ident $arr)) ids.back!
               `(Array.map (fun $(← mkTuple ids) => $(inner[0]!)) $arr)
           let arr ← if k == `sepBy then
             `(mkSepArray $arr $(getSepStxFromSplice arg))

src/Lean/Elab/Tactic/BuiltinTactic.lean

@@ -465,7 +465,7 @@ def renameInaccessibles (mvarId : MVarId) (hs : TSyntaxArray ``binderIdent) : Ta
         let inaccessible := !(extractMacroScopes localDecl.userName |>.equalScope callerScopes)
         let shadowed := found.contains localDecl.userName
         if inaccessible || shadowed then
-          if let `(binderIdent| $h:ident) := hs.back then
+          if let `(binderIdent| $h:ident) := hs.back! then
             let newName := h.getId
             lctx := lctx.setUserName localDecl.fvarId newName
             info := info.push (localDecl.fvarId, h)

src/Lean/Meta/ArgsPacker.lean

@@ -56,7 +56,7 @@ Given a telescope of FVars of type `tᵢ`, iterates `PSigma` to produce the type
 `t₁ ⊗' t₂ …`.
 -/
 def packType (xs : Array Expr) : MetaM Expr := do
-  let mut d ← inferType xs.back
+  let mut d ← inferType xs.back!
   for x in xs.pop.reverse do
     d ← mkAppOptM ``PSigma #[some (← inferType x), some (← mkLambdaFVars #[x] d)]
   return d
@@ -217,7 +217,7 @@ Helpers for iterated `PSum`.
 
 /-- Given types `#[t₁, t₂,…]`, returns the type `t₁ ⊕' t₂ …`. -/
 def packType (ds : Array Expr) : MetaM Expr := do
-  let mut r := ds.back
+  let mut r := ds.back!
   for d in ds.pop.reverse do
     r ← mkAppM ``PSum #[d, r]
   return r
@@ -335,7 +335,7 @@ def uncurryTypeND (types : Array Expr) : MetaM Expr := do
     unless type.isArrow do
       throwError "Mutual.uncurryTypeND: Expected non-dependent types, got {type}"
   let codomains := types.map (·.bindingBody!)
-  let t' := codomains.back
+  let t' := codomains.back!
   codomains.pop.forM fun t =>
     unless ← isDefEq t t' do
       throwError "Mutual.uncurryTypeND: Expected equal codomains, but got {t} and {t'}"

src/Lean/Meta/Closure.lean

@@ -239,7 +239,7 @@ def pickNextToProcess? : ClosureM (Option ToProcessElement) := do
     pure none
   else
     modifyGet fun s =>
-      let elem      := s.toProcess.back
+      let elem      := s.toProcess.back!
       let toProcess := s.toProcess.pop
       let (elem, toProcess) := pickNextToProcessAux lctx 0 toProcess elem
       (some elem, { s with toProcess := toProcess })

src/Lean/Meta/DiscrTree.lean

@@ -426,7 +426,7 @@ partial def mkPathAux (root : Bool) (todo : Array Expr) (keys : Array Key) (conf
   if todo.isEmpty then
     return keys
   else
-    let e    := todo.back
+    let e    := todo.back!
     let todo := todo.pop
     let (k, todo) ← pushArgs root todo e config noIndexAtArgs
     mkPathAux false todo (keys.push k) config noIndexAtArgs
@@ -603,7 +603,7 @@ private partial def getMatchLoop (todo : Array Expr) (c : Trie α) (result : Arr
     else if cs.isEmpty then
       return result
     else
-      let e     := todo.back
+      let e     := todo.back!
       let todo  := todo.pop
       let first := cs[0]! /- Recall that `Key.star` is the minimal key -/
       let (k, args) ← getMatchKeyArgs e (root := false) config
@@ -748,7 +748,7 @@ where
       else if cs.isEmpty then
         return result
       else
-        let e     := todo.back
+        let e     := todo.back!
         let todo  := todo.pop
         let (k, args) ← getUnifyKeyArgs e (root := false) config
         let visitStar (result : Array α) : MetaM (Array α) :=