t:AdjList. t.out 
t.size
(t.size List)
y ; b.l' list_accum(x,a.f(x;a);f(y;b);l') (recursive)T,T':Type, l:T List, y:T', f:(T'TT'). list_accum(x,a.f(x,a);y;l) T'A:Type, B:(AType), p:(a:A
B(a)). 2of(p) B(1of(p))| Who Cites adjl-edge-accum? | |
| adjl-edge-accum | Def adjl-edge-accum(A;s',x'.f(s';x');s;x) == list_accum(s',x'.f(s';x');s;A.out(x)) |
| adjl_out | Def t.out == 2of(t) |
| Thm* t:AdjList. t.out t.size(t.size List) | |
| list_accum | Def list_accum(x,a.f(x;a);y;l) == Case of l; nil y ; b.l' list_accum(x,a.f(x;a);f(y;b);l') (recursive) |
| Thm* T,T':Type, l:T List, y:T', f:(T'TT'). list_accum(x,a.f(x,a);y;l) T' | |
| pi2 | Def 2of(t) == t.2 |
| Thm* A:Type, B:(AType), p:(a:AB(a)). 2of(p) B(1of(p)) |
| Syntax: | adjl-edge-accum(A;s',x'.f(s';x');s;x) | has structure: | adjl-edge-accum(A; s',x'.f(s';x'); s; x) |
About:
 |  |  |  |  |
 |  |  |  |  |  |  |