| | Who Cites sublist 2? |
|
| sublist_2 | Def (  eq)(L,M) ==  x L.x(eq) M |
| | | Thm* T:Type, eq:(T  T ). (eq) (T List)(T List) |
|
| is_member | Def x(eq) L == (letrec is_member x eq L = (Case of L; nil  false ; h.t if eq(x,h) true else is_member(x,eq,t) fi) ) (x,eq,L) |
| | | Thm* T:Type, eq:(TT), u:T. u(eq) nil |
| | | Thm* T:Type, eq:(TT), x:T, L:T List. x(eq) L |
|
| list_all_2 | Def xL.P(x) == (letrec all L = (Case of L; nil true ; h.t P(h) (all(t))) ) (L) |
| | | Thm* T:Type, P:(T), L:T List. xL.P(x) |
|
| letrec_body | Def = b == b |
|
| letrec_arg | Def x b(x) (x) == b(x) |
|
| letrec | Def (letrec f b(f)) == b((letrec f b(f)) ) (recursive) |
|
| band | Def pq == if p q else false fi |
| | | Thm* p,q:. (pq) |
