Skip to content

Commit 4818a34

Browse files
Update Sublist.lean
1 parent 9d37f73 commit 4818a34

File tree

1 file changed

+1
-1
lines changed

1 file changed

+1
-1
lines changed

src/Init/Data/List/Sublist.lean

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -853,7 +853,7 @@ theorem isPrefix_iff_getElem {l₁ l₂ : List α} :
853853
| cons _ _ =>
854854
simp only [length_cons, Nat.add_le_add_iff_right, Fin.getElem_fin] at hl h
855855
simp only [cons_prefix_cons]
856-
exact ⟨h 0, tail_ih hl (fun a ↦ h a.succ)
856+
exact ⟨h 0, tail_ih hl fun a ↦ h a.succ⟩
857857

858858
-- See `Init.Data.List.Nat.Sublist` for `isSuffix_iff` and `ifInfix_iff`.
859859

0 commit comments

Comments
 (0)