Nuprl - Some Definitions

	Some definitions of interest.

iff	`Def P Q == (P Q) & (P Q)`

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

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

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

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`

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: