Nuprl - Some Definitions

	Some definitions of interest.

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'`

primrec	`Def primrec(n;b;c) == if n=0 b else c(n-1,primrec(n-1;b;c)) fi (recursive)`

	`Thm* T:Type, n:, b:T, c:(nTT). primrec(n;b;c) T`

top	`Def Top == Void given Void`

	`Thm* Top Type`

upto	`Def upto(i;j) == if i < j [i / upto(i+1;j)] else nil fi (recursive)`

	`Thm* i,j:. upto(i;j) {i..j} List`

About: