Setoid version of indexed containers.

[andreasabel]

Following the structure for non-indexed containers.

Putting this out for a first review.

I also added an Example development: multi-sorted algebras. This should be refactored after also adding a setoid version of Data.W.Indexed to the library.

Where in the hierachy would proofs be placed that the definitions in Data.W.Indexed are Funcs, i.e., respect setoid-equality?

[MatthewDaggitt]

@andreasabel if you would like this merged in for v2.0 please could you address the comments? Otherwise I'll mark it as abandoned.

[MatthewDaggitt]

Marking as abandoned and closing

[andreasabel]

Sorry for not getting back.

Our last status was that we disagreed on whether to use I -> Setoid or IndexedSetoid, and on this fundamental issue there was no resolve, so that PR is stuck.

[jamesmckinna]

And the distinction.conflict arising between the use of I -> Setoid or IndexedSetoid turns on two things, IIUC:

• [ ] the absence of a suitable function space between IndexedSetoids
• [ ] the contrast between explicit/implicit quantification over I in the two approaches

Can each of these be easily overcome? or is my question above about implicit eta-expansion one reason why the second issue is a deal-breaker?

[jamesmckinna]

I had promised, a loooong time ago, to try to understand (and fix) this, but it fell completely off my worklist. But I don't think we should abandon it (yet): v2.0 or v3.0?

[MatthewDaggitt]

Okay, brought this up to date. I no longer care so much about unifying the different versions of indexing so I propose to merge this in once the checks passed. Sorry for such a long wait @andreasabel

[MatthewDaggitt]

Eek still needs a changelog entry