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)
T:Type, eq:(T
T
), u:T. u(eq) nil T:Type, eq:(TT), x:T, L:T List. x(eq) L | Who Cites is member? | |
| 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 | |
| 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) |
| Syntax: | x(eq) L | has structure: | is_member(eq; x; L) |
About:
 |  |  |  |  |  |
 |  |  |  |  |  |  |
 |