Adrián García (Aug 23 2021 at 01:42): Adrián García (Aug 23 2021 at 01:42):My thesis advisor asked me to find the current work about lists and multisets in Coq's library for a bachelor's degree. Is looking at coq.inria.fr/library a good idea to start with or does someone knows an interesting line of research about it? Thanks!
Olivier Laurent (Aug 23 2021 at 06:48):This is a good starting point but alternative developments could also be found in other libraries:
https://github.com/coq/coq/wiki#coq-libraries
https://github.com/coq/stdlib2/wiki/Other-%22standard%22-libraries
Olivier Laurent (Aug 23 2021 at 06:55):Additional work on multisets:
http://color.inria.fr/doc/CoLoR.Util.Multiset.MultisetList.html
https://github.com/coq-contribs/fsets/blob/master/MultiSets.v
https://github.com/meta-logic/coq-ll/blob/master/PLL/LL/Multisets.v
https://github.com/olaure01/ollibs/blob/master/fmsetlist.v
Paolo Giarrusso (Aug 26 2021 at 03:43):I'll inline https://gitlab.mpi-sws.org/iris/stdpp/-/blob/master/theories/gmultiset.v even if stdpp is probably reachable from the above links
Last updated: Oct 13 2024 at 01:02 UTC