In Dafny, given a finite map, can I get its domain?

94 views Asked by At

I'm passed a finite map, m. Is there a way to compute its domain? Something like m.Domain, dom(m), etc. The reference manual doesn't say that there is such a function.

1

There are 1 answers

0
James Wilcox On BEST ANSWER

You can use m.Keys for that.

Unfortunately, this change is relatively recent, and the reference manual is out of date in this respect.

The Keys option is briefly mentioned in the release notes to version 1.9.9.