kframework - 如何检查键值对是否不在 kframework 的映射中?
问题描述
我写了类似的东西
requires notBool(K |-> V in P)
但这似乎不是正确的语法。检查映射中是否不存在键值对的正确方法是什么?
解决方案
您想要的语法是notBool K in_keys(P)
检查键是否在地图中。如果你还想检查键是否绑定到某个值,你可以写notBool K in_keys(P) orBool P[K] =/=K V
.
推荐阅读
- android - 下载文件后显示状态栏通知。| 安卓工作室
- blockly - 当我在 Blockly 中将任何 custom_block 作为 setcheck("position") 中的类型传递时,set Check 方法在语句输入中不起作用
- c# - 如何在 VSTO 的 Excel 状态栏中显示“更新工作流状态”进度条?
- python - 在 python 中是否有一个函数/模块可以替换文件中的所有变量?
- html - 需要帮助将文本集中在网格内的图像上
- android - 反应本机,屏幕方向不起作用
- node.js - Mongoose session.abortTransaction 不会回滚操作
- tensorflow - Tensorflow Probability (TFP):BNN 图像分类器不使用 OneHotCategorical 层学习
- python - 如何将1000变成1e3?
- c++ - xdevapi for MySQL 使用 c++ 连接器链接器问题