graph 1 3 Sections Graphs Doc

Def if b t else f fi == InjCase(b ; t; f)

is mentioned by

Def adjm-edge-accum(M;s',x'.f(s';x');s;x) == primrec(M.size;s;y,s'. if M.adj(x,y) f(s';y) else s' fi)[adjm-edge-accum]
Def dfs(the_obj;s;i) == if member-paren(x,y.the_obj.eq(x,y);i;s) s else [inl(i) / (the_obj.eacc((s',j. dfs(the_obj;s';j)),[inr(i) / s],i))] fi (recursive)[dfs]
Def vertex-subset(the_obj;x.P(x)) == the_obj.vacc((l,x. if P(x) [x / l] else l fi),nil)[vertex-subset]

In prior sections: bool 1 mb nat mb list 2 graph 1 1 graph 1 2 prog 1 int 2 list 1 mb list 1 num thy 1

Try larger context: Graphs

graph 1 3 Sections Graphs Doc