fix: broken docstring examples (#7526)

This PR fixes docstring breakage from #7516.
This commit is contained in:
David Thrane Christiansen 2025-03-17 18:59:03 +01:00 committed by GitHub
parent 5a5e83c26c
commit c53b0c99de
No known key found for this signature in database
GPG key ID: B5690EEEBB952194
2 changed files with 10 additions and 10 deletions

View file

@ -1451,25 +1451,25 @@ using `f` if the index is larger than the length of the List.
Examples:
```lean example
["circle", "square", "triangle"].modifyTailIdx List.reverse 1
["circle", "square", "triangle"].modifyTailIdx 1 List.reverse
```
```output
["circle", "triangle", "square"]
```
```lean example
["circle", "square", "triangle"].modifyTailIdx (fun xs => xs ++ xs) 1
["circle", "square", "triangle"].modifyTailIdx 1 (fun xs => xs ++ xs)
```
```output
["circle", "square", "triangle", "square", "triangle"]
```
```lean example
["circle", "square", "triangle"].modifyTailIdx (fun xs => xs ++ xs) 2
["circle", "square", "triangle"].modifyTailIdx 2 (fun xs => xs ++ xs)
```
```output
["circle", "square", "triangle", "triangle"]
```
```lean example
["circle", "square", "triangle"].modifyTailIdx (fun xs => xs ++ xs) 5
["circle", "square", "triangle"].modifyTailIdx 5 (fun xs => xs ++ xs)
```
```output
["circle", "square", "triangle"]
@ -1509,9 +1509,9 @@ Replaces the element at the given index, if it exists, with the result of applyi
index is invalid, the list is returned unmodified.
Examples:
* `[1, 2, 3].modify (· * 10) 0 = [10, 2, 3]`
* `[1, 2, 3].modify (· * 10) 2 = [1, 2, 30]`
* `[1, 2, 3].modify (· * 10) 3 = [1, 2, 3]`
* `[1, 2, 3].modify 0 (· * 10) = [10, 2, 3]`
* `[1, 2, 3].modify 2 (· * 10) = [1, 2, 30]`
* `[1, 2, 3].modify 3 (· * 10) = [1, 2, 3]`
-/
def modify (l : List α) (i : Nat) (f : αα) : List α :=
l.modifyTailIdx i (modifyHead f)

View file

@ -297,9 +297,9 @@ Replaces the element at the given index, if it exists, with the result of applyi
This is a tail-recursive version of `List.modify`.
Examples:
* `[1, 2, 3].modifyTR (· * 10) 0 = [10, 2, 3]`
* `[1, 2, 3].modifyTR (· * 10) 2 = [1, 2, 30]`
* `[1, 2, 3].modifyTR (· * 10) 3 = [1, 2, 3]`
* `[1, 2, 3].modifyTR 0 (· * 10) = [10, 2, 3]`
* `[1, 2, 3].modifyTR 2 (· * 10) = [1, 2, 30]`
* `[1, 2, 3].modifyTR 3 (· * 10) = [1, 2, 3]`
-/
def modifyTR (l : List α) (i : Nat) (f : αα) : List α := go l i #[] where
/-- Auxiliary for `modifyTR`: `modifyTR.go f l i acc = acc.toList ++ modify f i l`. -/