Hi. I'm looking for more documentation about finmap and finset. I know about https://github.com/math-comp/finmap/blob/master/finmap.v and have worked with that so far, but I feel like I'm struggling to prove basic things. If there are any tutorials on finmap and finset, please let me know. I'm particularly interested right now in understanding the finset implementation in mathcomp.finmap.

I wrote a short guide to the set part of these two libraries a while ago, and I just made it publicly available. It doesn't talk about the implementation of finset, but I don't think you should need to know about the implementation in order to be able to use the library (in fact, I don't know anything about it and I'm comfortable using the library).

Thank you @Ana de Almeida Borges. Your short guide is helpful to me :smile:

Last updated: Jul 15 2024 at 21:02 UTC