Email Gateway (Aug 18 2022 at 13:17): Email Gateway (Aug 18 2022 at 13:17):From: 游珍 <yucy0405@163.com>
The following are the part of context in dfs.thy.
subsection "Definition of Graphs"
typedecl node
types graph = "(node * node) list"
consts
nexts :: "[graph, node] \<Rightarrow> node list"
primrec
"nexts [] n = []"
"nexts (e#es) n = (if fst e = n then snd e # nexts es n else nexts es n)"
definition
nextss :: "[graph, node list] \<Rightarrow> node set" where
"nextss g xs = set g `` set xs"
I don't know the meaning of the operation in the "nextss g xs = set g set xs"?
yucy
Email Gateway (Aug 18 2022 at 13:17):From: Tobias Nipkow <nipkow@in.tum.de>
wrote:
The infix `` is the image of a relation over a set. It is defined in
Relation.thy.
Regards
Tobias
Last updated: Nov 04 2025 at 08:30 UTC