Nuprl - Some Definitions

	Some definitions of interest.

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`

assert	`Def b == if b True else False fi`

	`Thm* b:. b Prop`

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

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

l_before	`Def x before y l == [x; y] l`

	`Thm* T:Type, l:T List, x,y:T. x before y l Prop`

mapfilter	`Def mapfilter(f;P;L) == map(f;filter(P;L))`

	`Thm* T:Type, P:(T), T':Type, f:({x:T\| P(x) }T'), L:T List. mapfilter(f;P;L) T' List`

About: