Nuprl - Some Definitions

disjoint	`Def disjoint(eq;L1;L2) == xL1.x(eq) L2` `Thm* T:Type, eq:(TT), L1,L2:T List. disjoint(eq;L1;L2) Type`
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`
bnot	`Def b == if b false else true fi` `Thm* b:. b`
assert	`Def b == if b True else False fi` `Thm* b:. b Prop`
list_all	`Def xL.P(x) == (letrec list_all L = (Case of L; nil True ; h.t P(h) & list_all(t)) ) (L) Thm* T:Type, P:(TProp), L:T List. xL.P(x) Type` `Thm* T:Type, P:(TType). xnil.P(x) Type`
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)`

About: