From 54522006f4dac35ab184068693c7ef93ed629ea9 Mon Sep 17 00:00:00 2001
From: Sebastian Ullrich <sebasti@nullri.ch>
Date: Tue, 15 Feb 2022 18:39:15 +0100
Subject: [PATCH] refactor: List.get: take `Fin` to align with `Array.get`

/cc @leodemoura
---
 src/Init/Data/Array/Basic.lean       |  6 +++---
 src/Init/Prelude.lean                | 12 ++++++------
 src/Lean/Elab/Tactic/Conv/Congr.lean |  2 +-
 src/Lean/Meta/Match/Match.lean       |  4 ++--
 4 files changed, 12 insertions(+), 12 deletions(-)

diff --git a/src/Init/Data/Array/Basic.lean b/src/Init/Data/Array/Basic.lean
index d5a434ddcc..63460d9559 100644
--- a/src/Init/Data/Array/Basic.lean
+++ b/src/Init/Data/Array/Basic.lean
@@ -575,7 +575,7 @@ theorem ext (a b : Array α)
     : a = b := by
   let rec extAux (a b : List α)
       (h₁ : a.length = b.length)
-      (h₂ : (i : Nat) → (hi₁ : i < a.length) → (hi₂ : i < b.length) → a.get i hi₁ = b.get i hi₂)
+      (h₂ : (i : Nat) → (hi₁ : i < a.length) → (hi₂ : i < b.length) → a.get ⟨i, hi₁⟩ = b.get ⟨i, hi₂⟩)
       : a = b := by
     induction a generalizing b with
     | nil =>
@@ -590,11 +590,11 @@ theorem ext (a b : Array α)
         have hz₂ : 0 < (b::bs).length := by rw [List.length_cons]; apply Nat.zero_lt_succ
         have headEq : a = b := h₂ 0 hz₁ hz₂
         have h₁' : as.length = bs.length := by rw [List.length_cons, List.length_cons] at h₁; injection h₁; assumption
-        have h₂' : (i : Nat) → (hi₁ : i < as.length) → (hi₂ : i < bs.length) → as.get i hi₁ = bs.get i hi₂ := by
+        have h₂' : (i : Nat) → (hi₁ : i < as.length) → (hi₂ : i < bs.length) → as.get ⟨i, hi₁⟩ = bs.get ⟨i, hi₂⟩ := by
           intro i hi₁ hi₂
           have hi₁' : i+1 < (a::as).length := by rw [List.length_cons]; apply Nat.succ_lt_succ; assumption
           have hi₂' : i+1 < (b::bs).length := by rw [List.length_cons]; apply Nat.succ_lt_succ; assumption
-          have : (a::as).get (i+1) hi₁' = (b::bs).get (i+1) hi₂' := h₂ (i+1) hi₁' hi₂'
+          have : (a::as).get ⟨i+1, hi₁'⟩ = (b::bs).get ⟨i+1, hi₂'⟩ := h₂ (i+1) hi₁' hi₂'
           apply this
         have tailEq : as = bs := ih bs h₁' h₂'
         rw [headEq, tailEq]
diff --git a/src/Init/Prelude.lean b/src/Init/Prelude.lean
index 5967ad8dc1..e8a529dda3 100644
--- a/src/Init/Prelude.lean
+++ b/src/Init/Prelude.lean
@@ -1100,12 +1100,12 @@ def List.concat {α : Type u} : List α → α → List α
   | nil,       b => cons b nil
   | cons a as, b => cons a (concat as b)
 
-def List.get {α : Type u} : (as : List α) → (i : Nat) → LT.lt i as.length → α
-  | nil,       i,          h => absurd h (Nat.not_lt_zero _)
-  | cons a as, 0,          h => a
-  | cons a as, Nat.succ i, h =>
+def List.get {α : Type u} : (as : List α) → Fin as.length → α
+  | nil,       i      => absurd i.isLt (Nat.not_lt_zero _)
+  | cons a as, ⟨0, _⟩ => a
+  | cons a as, ⟨Nat.succ i, h⟩ =>
     have : LT.lt i.succ as.length.succ := length_cons .. ▸ h
-    get as i (Nat.le_of_succ_le_succ this)
+    get as ⟨i, Nat.le_of_succ_le_succ this⟩
 
 structure String where
   data : List Char
@@ -1205,7 +1205,7 @@ def Array.size {α : Type u} (a : @& Array α) : Nat :=
 
 @[extern "lean_array_fget"]
 def Array.get {α : Type u} (a : @& Array α) (i : @& Fin a.size) : α :=
-  a.data.get i.val i.isLt
+  a.data.get i
 
 @[inline] def Array.getD (a : Array α) (i : Nat) (v₀ : α) : α :=
   dite (LT.lt i a.size) (fun h => a.get ⟨i, h⟩) (fun _ => v₀)
diff --git a/src/Lean/Elab/Tactic/Conv/Congr.lean b/src/Lean/Elab/Tactic/Conv/Congr.lean
index 67268ba377..2137b205b0 100644
--- a/src/Lean/Elab/Tactic/Conv/Congr.lean
+++ b/src/Lean/Elab/Tactic/Conv/Congr.lean
@@ -70,7 +70,7 @@ private def selectIdx (tacticName : String) (mvarIds : List MVarId) (i : Int) :
       for mvarId in mvarIds, j in [:mvarIds.length] do
         if i != j then
           applyRefl mvarId
-      replaceMainGoal [mvarIds.get i h]
+      replaceMainGoal [mvarIds.get ⟨i, h⟩]
       return ()
   throwError "invalid '{tacticName}' conv tactic, application has only {mvarIds.length} (nondependent) argument(s)"
 
diff --git a/src/Lean/Meta/Match/Match.lean b/src/Lean/Meta/Match/Match.lean
index 75ed558f7b..06490386ed 100644
--- a/src/Lean/Meta/Match/Match.lean
+++ b/src/Lean/Meta/Match/Match.lean
@@ -595,7 +595,7 @@ private def moveToFront (p : Problem) (i : Nat) : Problem :=
   if i == 0 then
     p
   else if h : i < p.vars.length then
-    let x := p.vars.get i h
+    let x := p.vars.get ⟨i, h⟩
     { p with
       vars := List.moveToFront p.vars i
       alts := p.alts.map fun alt => { alt with patterns := List.moveToFront alt.patterns i }
@@ -662,7 +662,7 @@ where
     We only consider variables that do not depend on other variables at `p.vars`. -/
   findNext (i : Nat) : MetaM (Option Nat) := do
     if h : i < p.vars.length then
-      let x := p.vars.get i h
+      let x := p.vars.get ⟨i, h⟩
       if (← checkVarDeps p.vars i (← inferType x)) then
         return i
       else