Nuprl - Some Definitions

	Some definitions of interest.

reverse	`Def rev(as) == Case of as; nil nil ; a.as' rev(as') @ [a] (recursive)`

	`Thm* T:Type, as:T List. rev(as) T List`

append	`Def as @ bs == Case of as; nil bs ; a.as' [a / (as' @ bs)] (recursive)`

	`Thm* T:Type, as,bs:T List. (as @ bs) T List`

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

	`Thm* A,B:Prop. (A B) 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`

About: