Stream: Coq users

Topic: Partial maps and id's


view this post on Zulip Adrián García (Aug 07 2022 at 07:21):

Hello, anyone knows if there is a way to "loop through" a partial map? I'm following the Software Foundations implementation for partial maps. I used nat for id's, and I would like that given a partial map, return the min nat that has not been used in the map, so I need to at least get the id's that the map has already mapped.

view this post on Zulip Adrián García (Aug 07 2022 at 22:11):

What if instead of using a partial map, we use a pair of (partial map, list) so each time an update is made, store the value on the list to keep record of the entries?

view this post on Zulip Paolo Giarrusso (Aug 08 2022 at 08:15):

that’d support work, but it seems it might not be enough if you need to prove your map is well-behaved. Various libraries have alternative implementations of partial maps beyond SF’s K -> option V


Last updated: Jan 28 2023 at 07:30 UTC