问如何检查键值对是否不在kframework的映射中？
EN

Stack Overflow用户

提问于 2020-04-09 03:31:43

回答 1查看 28关注 0票数 0

我写了一些类似这样的东西

requires notBool(K |-> V in P)

但它似乎不是正确的语法。检查map中是否不存在键-值对的正确方法是什么？

发布于 2020-04-09 03:46:37

您想要的语法是notBool K in_keys(P)，用于检查键是否在映射中。如果您还想检查键是否绑定到某个值，可以编写notBool K in_keys(P) orBool P[K] =/=K V。

票数 1

页面原文内容由Stack Overflow提供。腾讯云小微IT领域专用引擎提供翻译支持

原文链接：

https://stackoverflow.com/questions/61108591

复制

相似问题

问如何检查键值对是否不在kframework的映射中？EN