Stream: math-comp users

Topic: Documentation and tutorial for finmap and finset


view this post on Zulip Ricardo (Jan 11 2023 at 05:07):

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.

view this post on Zulip Ana de Almeida Borges (Jan 11 2023 at 12:36):

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

view this post on Zulip Ricardo (Jan 12 2023 at 04:02):

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


Last updated: Jul 15 2024 at 21:02 UTC