Nuprl - Some Definitions

	Some definitions of interest.

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`

le	`Def AB == B < A`

	`Thm* i,j:. (ij) Prop`

not	`Def A == A False`

	`Thm* A:Prop. (A) Prop`

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: