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