def
definition
def or abbrev
reachable
show as:
view Lean formalization →
formal statement (Lean)
21def reachable (G : StakeGraph) (nodes : List Stakeholder) (src dst : Stakeholder) : Bool :=
proof body
Definition body.
22 let rec dfs (front : List Stakeholder) (visited : List Stakeholder) : Bool :=
23 match front with
24 | [] => False
25 | v :: vs =>
26 if decide (v = dst) then True else
27 let nbrs := neighbors G nodes v
28 let fresh := nbrs.filter (fun w => ¬ contains visited w)
29 dfs (vs ++ fresh) (v :: visited)
30 dfs [src] []
31