Project fails to compile on Agda 2.6.4

phijor / agda-cubical-multiset

(Finite) multisets in Cubical Agda

https://phijor.github.io/agda-cubical-multiset/README.html

MIT License

7 stars 0 forks source link

Project fails to compile on Agda 2.6.4 #1

Open pufferffish opened 6 months ago

pufferffish commented 6 months ago

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 commented 6 months ago

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 :)