首页 > 解决方案 > 如何检查键值对是否不在 kframework 的映射中?

问题描述

我写了类似的东西

requires notBool(K |-> V in P)

但这似乎不是正确的语法。检查映射中是否不存在键值对的正确方法是什么?

标签: kframework

解决方案


您想要的语法是notBool K in_keys(P)检查键是否在地图中。如果你还想检查键是否绑定到某个值,你可以写notBool K in_keys(P) orBool P[K] =/=K V.


推荐阅读