functional-programming - Isabelle 标记图定义
问题描述
我正在尝试在 Isabelle HOL 中定义一些顶点标签,并且后继定义存在问题:
record ('v,'w) graph =
nodes :: "('v×'w) set"
edges :: "(('v×'w) × ('v×'w)) set"
definition succ :: "('v,'w) graph ⇒'v ⇒ ('v,'w) set"
where "succ G v ≡ {(v',w). ((v,w),(v',w))∈edges G}"
它说“类型构造函数的参数数量错误:“Set.set””,有人知道如何解决这个问题吗?
解决方案
succ
应该可能返回一组顶点标签对'v × 'w
,所以想写
definition succ :: "('v,'w) graph ⇒'v ⇒ ('v × 'w) set"
推荐阅读
- android - 在 Android 后台通知到达时增加通知量
- ansible - 有没有一种方法可以将 Ansible 断言函数与 YAML 文件中的项目而不是列表进行比较?
- java - JGit 抛出 org.eclipse.jgit.errors.MissingObjectException
- python - 导入简单的变压器
- json - 在 Windows 中使用 CURL 调用 Check_MK Web API 时“缺少必需的密钥”
- asp.net-mvc - 在 Chrome 上单击“提交”按钮时操作方法会触发两次
- c# - 如何同时调用Windows服务中的两个方法C#
- c# - IQueryable 可以用于内存中的集合吗?
- react-native - 在 kurento 中传递视频如何反应原生
- php - 流明队列突然中断