Skip to content

Commit

Permalink
feat(list): add map_with_index to core library (#259)
Browse files Browse the repository at this point in the history
I needed to use this in the widget implementation and it seems like
something basic enough to belong in core anyway.

Co-authored-by: Ed Ayers <EdAyers@users.noreply.github.com>
  • Loading branch information
EdAyers and EdAyers committed May 23, 2020
1 parent a74f982 commit a13a294
Showing 1 changed file with 9 additions and 0 deletions.
9 changes: 9 additions & 0 deletions library/init/data/list/basic.lean
Expand Up @@ -116,6 +116,15 @@ def reverse : list α → list α :=
| _ [] := []
| (x::xs) (y::ys) := f x y :: map₂ xs ys

def map_with_index_core (f : ℕ → α → β) : ℕ → list α → list β
| k [] := []
| k (a::as) := f k a::(map_with_index_core (k+1) as)

/-- Given a function `f : ℕ → α → β` and `as : list α`, `as = [a₀, a₁, ...]`, returns the list
`[f 0 a₀, f 1 a₁, ...]`. -/
def map_with_index (f : ℕ → α → β) (as : list α) : list β :=
map_with_index_core f 0 as

def join : list (list α) → list α
| [] := []
| (l :: ls) := l ++ join ls
Expand Down

0 comments on commit a13a294

Please sign in to comment.