Project fails to compile on Agda 2.6.4

[pufferffish]

The project currently cannot be built in Agda 2.6.3 and 2.6.4. The following error would occur:

This is because in Agda 2.6.3 they introduced the UnsupportedIndexedMatch warning.

The warning occurs becase the membership proof for list is defined using indexed types. I have an alternative definition of membership proofs that doesn't require indexed types here using the universal property of commutative monoids.

[phijor]

Hey, thanks for letting me know! I pushed an update to Agda 2.6.4 and cubical v0.6 to https://github.com/phijor/agda-cubical-multiset/tree/update-agda

It's not a proper fix yet, it simply disables the UnsupportedIndexedMatch warning. I'll have a look at your definition and see what I can incorporate! Thanks again, much appreciated :)