我正在尝试在 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””,有人知道如何解决这个问题吗?