Nuprl - Some Definitions

	Some definitions of interest.

l_member	`Def (x l) == i:. i < \|\|l\|\| & x = l[i] T`

	`Thm* T:Type, x:T, l:T List. (x l) Prop`

paren	`Def paren(T;s) == s = nil (T+T) List (t:T, s':(T+T) List. s = ([inl(t)] @ s' @ [inr(t)]) & paren(T;s')) (s',s'':(T+T) List. \|\|s'\|\| < \|\|s\|\| & \|\|s''\|\| < \|\|s\|\| & s = (s' @ s'') & paren(T;s') & paren(T;s'')) (recursive)`

	`Thm* T:Type, s:(T+T) List. paren(T;s) Prop`

About: