chore: robustify for byAsSorry (#892)

leanprover-community · Jul 26, 2024 · e789780 · e789780
1 parent d2b1546
commit e789780
Show file tree

Hide file tree

Showing 2 changed files with 2 additions and 2 deletions.
diff --git a/Batteries/CodeAction/Deprecated.lean b/Batteries/CodeAction/Deprecated.lean
@@ -32,7 +32,7 @@ def deprecatedCodeActionProvider : CodeActionProvider := fun params snap => do
   for m in snap.msgLog.toList do
     if m.data.isDeprecationWarning then
       if h : _ then
-        msgs := msgs.push (snap.cmdState.messages.toList[i])
+        msgs := msgs.push (snap.cmdState.messages.toList[i]'h)
     i := i + 1
   if msgs.isEmpty then return #[]
   let start := doc.meta.text.lspPosToUtf8Pos params.range.start

diff --git a/Batteries/Data/List/Lemmas.lean b/Batteries/Data/List/Lemmas.lean
@@ -379,7 +379,7 @@ theorem modifyNth_eq_take_drop (f : α → α) :
     ∀ n l, modifyNth f n l = take n l ++ modifyHead f (drop n l) :=
   modifyNthTail_eq_take_drop _ rfl
 
-theorem modifyNth_eq_take_cons_drop (f : α → α) {n l} (h) :
+theorem modifyNth_eq_take_cons_drop (f : α → α) {n l} (h : n < length l) :
     modifyNth f n l = take n l ++ f l[n] :: drop (n + 1) l := by
   rw [modifyNth_eq_take_drop, drop_eq_getElem_cons h]; rfl