Skip to content

Commit

Permalink
chore: fix List.modify/insertIdx doc-strings (#1006)
Browse files Browse the repository at this point in the history
  • Loading branch information
kim-em authored Oct 21, 2024
1 parent dd6b101 commit 7c5548e
Showing 1 changed file with 3 additions and 3 deletions.
6 changes: 3 additions & 3 deletions Batteries/Data/List/Basic.lean
Original file line number Diff line number Diff line change
Expand Up @@ -167,7 +167,7 @@ Split a list at every occurrence of a separator element. The separators are not
Apply a function to the nth tail of `l`. Returns the input without
using `f` if the index is larger than the length of the List.
```
modifyNthTail f 2 [a, b, c] = [a, b] ++ f [c]
modifyTailIdx f 2 [a, b, c] = [a, b] ++ f [c]
```
-/
@[simp] def modifyTailIdx (f : List α → List α) : Nat → List α → List α
Expand Down Expand Up @@ -220,9 +220,9 @@ theorem modifyTR_go_eq : ∀ l n, modifyTR.go f l n acc = acc.toList ++ modify f
| x :: xs, acc => go xs (acc.push x)

/--
`insertNth n a l` inserts `a` into the list `l` after the first `n` elements of `l`
`insertIdx n a l` inserts `a` into the list `l` after the first `n` elements of `l`
```
insertNth 2 1 [1, 2, 3, 4] = [1, 2, 1, 3, 4]
insertIdx 2 1 [1, 2, 3, 4] = [1, 2, 1, 3, 4]
```
-/
def insertIdx (n : Nat) (a : α) : List α → List α :=
Expand Down

0 comments on commit 7c5548e

Please sign in to comment.