chore: bump toolchain to 4.16.0-rc1 (#262)

examples/website-examples/lake-manifest.json

@@ -4,7 +4,7 @@
  [{"url": "https://github.com/leanprover/subverso.git",
    "type": "git",
    "subDir": null,
-   "rev": "6e2fe670be67ad4e31c7b0ad0fe7141e59bd1d29",
+   "rev": "844b9a53cf7acd71e0e81a3a56608bb28215646d",
    "name": "subverso",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",

lake-manifest.json

@@ -15,7 +15,7 @@
    "type": "git",
    "subDir": null,
    "scope": "",
-   "rev": "6e2fe670be67ad4e31c7b0ad0fe7141e59bd1d29",
+   "rev": "844b9a53cf7acd71e0e81a3a56608bb28215646d",
    "name": "subverso",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",

lean-toolchain

@@ -1 +1 @@
-leanprover/lean4:v4.15.0
+leanprover/lean4:v4.16.0-rc1

src/verso-blog/VersoBlog.lean

@@ -120,7 +120,7 @@ def NameSuffixMap.insert (map : NameSuffixMap α) (key : Name) (val : α) : Name
     | map
   let mut arr := map.contents.find? last |>.getD #[]
   for h : i in [0:arr.size] do
-    have : i < arr.size := by cases h; simp [*]
+    have : i < arr.size := by get_elem_tactic
     if arr[i].fst == key then
       return {map with contents := map.contents.insert last (arr.set i (key, val))}
   return {map with contents := map.contents.insert last (arr.push (key, val))}

src/verso/Verso/Code/Highlighted.lean

@@ -332,13 +332,13 @@ where
 def _root_.Array.mapIndexed (arr : Array α) (f : Fin arr.size → α → β) : Array β := Id.run do
   let mut out := #[]
   for h : i in [:arr.size] do
-    out := out.push (f ⟨i, h.right⟩ arr[i])
+    out := out.push (f ⟨i, by get_elem_tactic⟩ arr[i])
   out
 
 def _root_.Array.mapIndexedM [Monad m] (arr : Array α) (f : Fin arr.size → α → m β) : m (Array β) := do
   let mut out := #[]
   for h : i in [:arr.size] do
-    out := out.push (← f ⟨i, h.right⟩ arr[i])
+    out := out.push (← f ⟨i, by get_elem_tactic⟩ arr[i])
   pure out
 
 

src/verso/Verso/Doc.lean

@@ -40,8 +40,9 @@ private def arrayEq (eq : α → α → Bool) (xs ys : Array α) : Bool := Id.ru
     if h : xs.size = ys.size then
       for h' : i in [0:xs.size] do
         have : i < ys.size := by
-          let ⟨_, h''⟩ := h'
-          simp [*] at h''; assumption
+          have : i < xs.size := by get_elem_tactic
+          rw [← h]
+          assumption
         if !(eq xs[i] ys[i]) then return false
       return true
     else return false

src/verso/Verso/Doc/ArgParse.lean

@@ -186,7 +186,7 @@ def ValDesc.resolvedName : ValDesc m Name where
     | .name x => realizeGlobalConstNoOverloadWithInfo x
     | other => throwError "Expected string, got {repr other}"
 
-def ArgParse.run [Monad m] [MonadInfoTree m] [MonadResolveName m] [MonadEnv m] [MonadError m] [MonadLiftT IO m] (p : ArgParse m α) (args : Array Arg) : m α := do
+def ArgParse.run [Monad m] [MonadInfoTree m] [MonadResolveName m] [MonadEnv m] [MonadError m] [MonadLiftT BaseIO m] (p : ArgParse m α) (args : Array Arg) : m α := do
   match ← p.parse _ ⟨args, #[]⟩ with
   | (.ok v, ⟨more, info⟩) =>
     if more.size = 0 then

src/verso/Verso/Hover.lean

@@ -32,7 +32,7 @@ structure CustomHover where
   markedString : String
 deriving TypeName
 
-def addCustomHover [Monad m] [MonadInfoTree m] [MonadLiftT IO m] (stx : Syntax) (hover : UserHover) : m Unit := do
+def addCustomHover [Monad m] [MonadInfoTree m] [MonadLiftT BaseIO m] (stx : Syntax) (hover : UserHover) : m Unit := do
   let txt ← match hover with
     | .markdown str => pure str
     | .messageData m => m.toString