Skip to content

GitLab

Closed
Created by Janno@jannoMaintainer

Wish: Prelude support for currying (and other operations) on gmap.

The following operations would (or could) be quite useful in my planned clean-up of iGPS:

  1. Converting gmap A (gmap B C) to gmap (A* B) (C) and vice versa.
  2. Converting gmap A B to gmap A (A * B) by copying the argument.
  3. Converting gmap A B as a gset (A * B) (possibly by simply adding a ElemOf instance and corresponding lemma).

As Robbert already mentioned to me, these things probably should be generalized. I think there is a general map-filter function lurking in there somewhere. One that gives access to both the key and the value and returns and optional results which is used for the new gmap. I might be wrong though.