take pairs

Stream: Is there code for X?

[Alex J. Best]

Does this have a name or is it already developed somewhere in mathlib, I guess it is really a combination of "pair up" and map

def take_pairs {α β : Type*} (f : α → α → β) : list α → list β
| [] := []
| [a] := []
| (a :: b :: l) := f a b :: take_pairs (b :: l)

[Yakov Pechersky]

Sorry, misunderstood

[Yakov Pechersky]

import data.list.zip

def take_pairs {α β : Type*} (f : α → α → β) : list α → list β
| [] := []
| [a] := []
| (a :: b :: l) := f a b :: take_pairs (b :: l)

def take_pairs' {α β : Type*} (f : α → α → β) (l : list α) : list β :=
list.zip_with f l l.tail

[Yakov Pechersky]

import data.list.zip

def take_pairs {α β : Type*} (f : α → α → β) : list α → list β
| [] := []
| [a] := []
| (a :: b :: l) := f a b :: take_pairs (b :: l)

def take_pairs' {α β : Type*} (f : α → α → β) (l : list α) : list β :=
list.zip_with f l l.tail

lemma tp_eq {α β : Type*} {f : α → α → β} {l : list α} : take_pairs f l = take_pairs' f l :=
begin
  induction l with hd tl IH,
  { refl },
  { cases tl,
    { refl },
    { simpa only [take_pairs, IH] } }
end

[Yakov Pechersky]

I might define a separate chunk_pairs as such:

def chunk_pairs {α β : Type*} (f : α → α → β) : list α → list β
| [] := []
| [a] := []
| (a :: b :: l) := f a b :: chunk_pairs l

[Adam Topaz]

What does hoogle say?

[Adam Topaz]

Looks like
https://hackage.haskell.org/package/utility-ht-0.0.15/docs/Data-List-HT.html#v:mapAdjacent

[Bhavik Mehta]

In Haskell I'd use zipWith f <*> tail

[Alex J. Best]

Awesome, thanks everyone!

[Eric Wieser]

docs#list.chain looks related but not what you're after