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

Question

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.

Answer 1

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.