dafny - 在 Dafny 中，给定一个有限映射，我可以得到它的域吗？

Question

我通过了一个有限的地图，米。有没有办法计算它的域？m.Domain、dom(m) 之类的东西。参考手册并没有说有这样的功能。

Answer 1

你可以使用m.Keys它。

不幸的是，这种变化是相对较新的，参考手册在这方面已经过时了。

版本 1.9.9Keys的发行说明中简要提到了该选项。