Nuprl - Some Definitions

	Some definitions of interest.

adjl_size	`Def t.size == 1of(t)`

	`Thm* t:AdjList. t.size`

adjlist	`Def AdjList == size:size(size List)`

	`Thm* AdjList Type`

int_seg	`Def {i..j} == {k:\| i k < j }`

	`Thm* m,n:. {m..n} Type`

no_repeats	`Def no_repeats(T;l) == i,j:. i < \|\|l\|\| j < \|\|l\|\| i = j l[i] = l[j] T`

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

nat	`Def == {i:\| 0i }`

	`Thm* 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: