如何解决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"
版权声明：本文内容由互联网用户自发贡献，该文观点与技术仅代表作者本人。本站仅提供信息存储空间服务，不拥有所有权，不承担相关法律责任。如发现本站有涉嫌侵权/违法违规的内容， 请发送邮件至 dio@foxmail.com 举报，一经查实，本站将立刻删除。
