def
definition
mutualReachable
show as:
view math explainer →
open explainer
Generate a durable explainer page for this declaration.
open lean source
IndisputableMonolith.Ethics.StakeGraph on GitHub at line 32.
browse module
All declarations in this module, on Recognition.
explainer page
depends on
used by
formal source
29 dfs (vs ++ fresh) (v :: visited)
30 dfs [src] []
31
32def mutualReachable (G : StakeGraph) (nodes : List Stakeholder) (s t : Stakeholder) : Bool :=
33 reachable G nodes s t && reachable G nodes t s
34
35def hasCycle (G : StakeGraph) (nodes : List Stakeholder) : Bool :=
36 nodes.any (fun s => G.edge s s)
37 || nodes.any (fun s =>
38 nodes.any (fun t => (¬ decide (s = t)) && mutualReachable G nodes s t))
39
40end StakeGraph
41end Ethics
42end IndisputableMonolith
43