CODEWITHSUNDEEP
functional-programmingisabellehol
Eva
Eva

Reputation: 35

Isabelle labeled graph definition

I am trying to define some vertex labels in Isabelle HOL and have a problem with the successor definition:

  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}"

It says "Bad number of arguments for type constructor: "Set.set"", does anyone know how to fix this?

Upvotes: 0

Views: 134

Answers (1)

Andreas Lochbihler
Andreas Lochbihler

Reputation: 5058

succ shall probably return a set of vertex-label pairs 'v × 'w, so want to write

definition succ :: "('v,'w) graph ⇒'v ⇒ ('v × 'w) set"

Upvotes: 1

Related Questions