list.blend

Stream: Is there code for X?

[Rob Lewis]

Does this function exist already? If not, what's the appropriate name?

def list.blend_aux {α β} (f : α → list α → β) : list α → list α → list β
| prev [] := []
| prev (h::t) := f h (prev++t) :: list.blend_aux (prev++[h]) t

def list.blend {α β} (f : α → list α → β) (l : list α) : list β :=
list.blend_aux f [] l

Basically: given f : α → list α → β, map f over a list l such that for each e in l, we compute f e l' where l' is l with e removed.

[Rob Lewis]

Use case: imagine you have a list of hypotheses l. You want so simplify each hypothesis h using all of the other hypotheses as simp rules, but you don't want to use h itself as a simp rule since that will just produce true. So if f: expr → list expr → expris "simplify an expr using these exprs as simp rules," we want to do l.blend f.

[Yaël Dillies]

For having roamed the list files recently, pretty sure we don't.

[Scott Morrison]

I recently needed something slightly more general with f : list A -> A -> list A, where the arguments represent a prefix of the list, the next element, and the suffix.

[Scott Morrison]

Then blend comes from concatenating the prefix and suffix.

[Scott Morrison]

That could be called map_with_prefix_suffix? Your version could be called map_with_complement?